:: BVFUNC_1 semantic presentation

definition
let c1, c2 be boolean set ;
func a1 'imp' a2 -> set equals :: BVFUNC_1:def 1
('not' a1) 'or' a2;
correctness
coherence
('not' c1) 'or' c2 is set ;
;
func a1 'eqv' a2 -> set equals :: BVFUNC_1:def 2
 'not' (a1 'xor' a2);
correctness
coherence
'not' (c1 'xor' c2) is set ;
;
commutativity
for b1 being set
for b2, b3 being boolean set holds
( b1 = 'not' (b2 'xor' b3) implies b1 = 'not' (b3 'xor' b2) ) ;
end;

:: deftheorem defines 'imp' BVFUNC_1:def 1 :
for b1, b2 being boolean set holds b1 'imp' b2 = ('not' b1) 'or' b2;

:: deftheorem defines 'eqv' BVFUNC_1:def 2 :
for b1, b2 being boolean set holds b1 'eqv' b2 = 'not' (b1 'xor' b2);

registration
let c1, c2 be boolean set ;
cluster a1 'imp' a2 -> boolean ;
correctness
coherence
c1 'imp' c2 is boolean;
proof
c1 'imp' c2 = ('not' c1) 'or' c2 ;
hence c1 'imp' c2 is boolean ;
end;
cluster a1 'eqv' a2 -> boolean ;
correctness
coherence
c1 'eqv' c2 is boolean;
proof
c1 'eqv' c2 = 'not' (c1 'xor' c2) ;
hence c1 'eqv' c2 is boolean ;
end;
end;

registration
cluster boolean -> natural set ;
coherence
for b1 being set holds
( b1 is boolean implies b1 is natural )
proof
let c1 be set ;
assume c1 is boolean ;
then c1 in BOOLEAN by MARGREL1:def 15;
hence c1 is natural by MARGREL1:def 12, TARSKI:def 2;
end;
end;

notation
let c1, c2 be boolean set ;
end;

definition
let c1, c2 be boolean set ;
means :E1: :: BVFUNC_1:def 3
a1 'imp' a2 = TRUE ;
compatibility
( c1 '<' c2 iff c1 'imp' c2 = TRUE )
proof
E1: ( c1 = 0 or c1 = 1 ) by MARGREL1:36, MARGREL1:39;
E2: ( c2 = 0 or c2 = 1 ) by MARGREL1:36, MARGREL1:39;
( ('not' c1) 'or' c2 = TRUE iff not ( not ( c1 = TRUE & c2 = TRUE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = FALSE & c2 = FALSE ) ) )
proof
E3: ( not ( not ( c1 = TRUE & c2 = TRUE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = FALSE & c2 = FALSE ) ) implies ('not' c1) 'or' c2 = TRUE )
proof
( ( c1 = FALSE & c2 = FALSE ) implies ( ('not' c1) 'or' c2 = TRUE ) )
proof
assume ( c1 = FALSE & c2 = FALSE ) ;
then 'not' c1 = TRUE by MARGREL1:def 16;
hence ('not' c1) 'or' c2 = TRUE by BINARITH:19;
end;
hence ( not ( not ( c1 = TRUE & c2 = TRUE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = FALSE & c2 = FALSE ) ) implies ('not' c1) 'or' c2 = TRUE ) by BINARITH:19;
end;
E4: not ( ('not' c1) 'or' c2 = TRUE & not 'not' c1 = TRUE & not c2 = TRUE )
proof
assume E5: ('not' c1) 'or' c2 = TRUE ;
('not' c1) 'or' c2 = 'not' (('not' ('not' c1)) '&' ('not' c2)) by BINARITH:def 1;
then 'not' (c1 '&' ('not' c2)) = TRUE by E5, MARGREL1:40;
then c1 '&' ('not' c2) = FALSE by MARGREL1:41;
then ( c1 = FALSE or 'not' c2 = FALSE ) by MARGREL1:45;
hence not ( not 'not' c1 = TRUE & not c2 = TRUE ) by MARGREL1:41;
end;
( not ( ( 'not' c1 = TRUE or c2 = TRUE ) & not ( c1 = TRUE & c2 = TRUE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = FALSE & c2 = FALSE ) ) & not ( not ( not ( c1 = TRUE & c2 = TRUE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = FALSE & c2 = FALSE ) ) & not 'not' c1 = TRUE & not c2 = TRUE ) ) by MARGREL1:39, MARGREL1:41;
hence ( ('not' c1) 'or' c2 = TRUE iff not ( not ( c1 = TRUE & c2 = TRUE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = FALSE & c2 = FALSE ) ) ) by E3, E4;
end;
hence ( c1 '<' c2 iff c1 'imp' c2 = TRUE ) by E1, E2, MARGREL1:36;
end;
end;

:: deftheorem E1 defines '<' BVFUNC_1:def 3 :
for b1, b2 being boolean set holds
( b1 '<' b2 iff b1 'imp' b2 = TRUE );

definition
let c1 be set ;
func BVF a1 -> set equals :: BVFUNC_1:def 4
 Funcs a1,BOOLEAN ;
correctness
coherence
Funcs c1,BOOLEAN is set ;
;
end;

:: deftheorem defines BVF BVFUNC_1:def 4 :
for b1 being set holds BVF b1 = Funcs b1,BOOLEAN ;

registration
let c1 be set ;
cluster BVF a1 -> non empty functional ;
coherence
( BVF c1 is functional & not BVF c1 is empty )
proof
BVF c1 = Funcs c1,BOOLEAN ;
hence BVF c1 is functional ;
thus not BVF c1 is empty ;
end;
end;

registration
let c1 be set ;
cluster -> boolean-valued Element of BVF a1;
coherence
for b1 being Element of BVF c1 holds b1 is boolean-valued
proof
let c2 be Element of BVF c1;
BVF c1 = Funcs c1,BOOLEAN ;
hence rng c2 c= BOOLEAN by FUNCT_2:169; :: uses VALUAT_1:def 2
end;
end;

notation
let c1 be boolean-valued Function;
let c2 be set ;
end;

scheme :: BVFUNC_1:sch 1
s1{ F1() -> non empty set , F2() -> Element of Funcs F1(),BOOLEAN , F3() -> Element of Funcs F1(),BOOLEAN , F4( set , Element of Funcs F1(),BOOLEAN , Element of Funcs F1(),BOOLEAN ) -> set } :
for b1, b2 being Element of Funcs F1(),BOOLEAN holds
( ( for b3 being Element of F1() holds Pj b1,b3 = F4(b3,F2(),F3()) & for b3 being Element of F1() holds Pj b2,b3 = F4(b3,F2(),F3()) ) implies ( b1 = b2 ) )
provided
proof
let c1, c2 be Element of Funcs F1(),BOOLEAN ;
assume that E2: for b1 being Element of F1() holds Pj c1,b1 = F4(b1,F2(),F3())
and E3: for b1 being Element of F1() holds Pj c2,b1 = F4(b1,F2(),F3()) ;
consider c3 being Function such that
E4: ( c1 = c3 & dom c3 = F1() & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E5: ( c2 = c4 & dom c4 = F1() & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in F1() implies Pj c3,b1 = Pj c4,b1 )
proof
let c5 be set ;
assume c5 in F1() ;
then reconsider c6 = c5 as Element of F1() ;
Pj c2,c6 = F4(c6,F2(),F3()) by E3;
hence Pj c3,c5 = Pj c4,c5 by E2, E4, E5;
end;
hence c1 = c2 by E4, E5, FUNCT_1:9;
end;

scheme :: BVFUNC_1:sch 2
s2{ F1() -> non empty set , F2( set ) -> set } :
for b1, b2 being Element of Funcs F1(),BOOLEAN holds
( ( for b3 being Element of F1() holds Pj b1,b3 = F2(b3) & for b3 being Element of F1() holds Pj b2,b3 = F2(b3) ) implies ( b1 = b2 ) )
provided
proof
let c1, c2 be Element of Funcs F1(),BOOLEAN ;
assume that E2: for b1 being Element of F1() holds Pj c1,b1 = F2(b1)
and E3: for b1 being Element of F1() holds Pj c2,b1 = F2(b1) ;
consider c3 being Function such that
E4: ( c1 = c3 & dom c3 = F1() & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E5: ( c2 = c4 & dom c4 = F1() & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in F1() implies Pj c3,b1 = Pj c4,b1 )
proof
let c5 be set ;
assume c5 in F1() ;
then reconsider c6 = c5 as Element of F1() ;
Pj c2,c6 = F2(c6) by E3;
hence Pj c3,c5 = Pj c4,c5 by E2, E4, E5;
end;
hence c1 = c2 by E4, E5, FUNCT_1:9;
end;

definition
let c1 be non empty set ;
let c2 be Element of BVF c1;
redefine func 'not' as 'not' a2 -> Element of BVF a1;
coherence
'not' c2 is Element of BVF c1
proof
reconsider c3 = c2 as Element of Funcs c1,BOOLEAN ;
'not' c3 is Element of Funcs c1,BOOLEAN ;
hence 'not' c2 is Element of BVF c1 ;
end;
let c3 be Element of BVF c1;
redefine func '&' as a2 '&' a3 -> Element of BVF a1;
coherence
c2 '&' c3 is Element of BVF c1
proof
reconsider c4 = c2, c5 = c3 as Element of Funcs c1,BOOLEAN ;
c4 '&' c5 is Element of Funcs c1,BOOLEAN ;
hence c2 '&' c3 is Element of BVF c1 ;
end;
end;

definition
let c1, c2 be boolean-valued Function;
func a1 'or' a2 -> Function means :E2: :: BVFUNC_1:def 5
( dom a3 = (dom a1) /\ (dom a2) & for b1 being set holds
( b1 in dom a3 implies Pj a3,b1 = (Pj a1,b1) 'or' (Pj a2,b1) ) );
existence
ex b1 being Function st
( dom b1 = (dom c1) /\ (dom c2) & for b2 being set holds
( b2 in dom b1 implies Pj b1,b2 = (Pj c1,b2) 'or' (Pj c2,b2) ) )
proof
deffunc H1( set ) -> set = (Pj c1,a1) 'or' (Pj c2,a1);
consider c3 being Function such that
E2: dom c3 = (dom c1) /\ (dom c2)
and E3: for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies Pj c3,b1 = H1(b1) ) from FUNCT_1:sch 3();
 take c3 ;
thus ( dom c3 = (dom c1) /\ (dom c2) & for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'or' (Pj c2,b1) ) ) by E2, E3;
end;
uniqueness
for b1, b2 being Function holds
( ( dom b1 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b1 implies Pj b1,b3 = (Pj c1,b3) 'or' (Pj c2,b3) ) & dom b2 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b2 implies Pj b2,b3 = (Pj c1,b3) 'or' (Pj c2,b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Function;
assume that E2: dom c3 = (dom c1) /\ (dom c2)
and E3: for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'or' (Pj c2,b1) )
and E4: dom c4 = (dom c1) /\ (dom c2)
and E5: for b1 being set holds
( b1 in dom c4 implies Pj c4,b1 = (Pj c1,b1) 'or' (Pj c2,b1) ) ;
for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = Pj c4,b1 )
proof
let c5 be set ;
assume c5 in dom c3 ;
then ( Pj c3,c5 = (Pj c1,c5) 'or' (Pj c2,c5) & Pj c4,c5 = (Pj c1,c5) 'or' (Pj c2,c5) ) by E2, E3, E4, E5;
hence Pj c3,c5 = Pj c4,c5 ;
end;
hence c3 = c4 by E2, E4, FUNCT_1:9;
end;
commutativity
for b1 being Function
for b2, b3 being boolean-valued Function holds
( ( dom b1 = (dom b2) /\ (dom b3) & for b4 being set holds
( b4 in dom b1 implies Pj b1,b4 = (Pj b2,b4) 'or' (Pj b3,b4) ) ) implies ( ( dom b1 = (dom b3) /\ (dom b2) & for b4 being set holds
( b4 in dom b1 implies Pj b1,b4 = (Pj b3,b4) 'or' (Pj b2,b4) ) ) ) ) ;
func a1 'xor' a2 -> Function means :E3: :: BVFUNC_1:def 6
( dom a3 = (dom a1) /\ (dom a2) & for b1 being set holds
( b1 in dom a3 implies Pj a3,b1 = (Pj a1,b1) 'xor' (Pj a2,b1) ) );
existence
ex b1 being Function st
( dom b1 = (dom c1) /\ (dom c2) & for b2 being set holds
( b2 in dom b1 implies Pj b1,b2 = (Pj c1,b2) 'xor' (Pj c2,b2) ) )
proof
deffunc H1( set ) -> set = (Pj c1,a1) 'xor' (Pj c2,a1);
consider c3 being Function such that
E2: dom c3 = (dom c1) /\ (dom c2)
and E3: for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies Pj c3,b1 = H1(b1) ) from FUNCT_1:sch 3();
 take c3 ;
thus ( dom c3 = (dom c1) /\ (dom c2) & for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'xor' (Pj c2,b1) ) ) by E2, E3;
end;
uniqueness
for b1, b2 being Function holds
( ( dom b1 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b1 implies Pj b1,b3 = (Pj c1,b3) 'xor' (Pj c2,b3) ) & dom b2 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b2 implies Pj b2,b3 = (Pj c1,b3) 'xor' (Pj c2,b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Function;
assume that E2: dom c3 = (dom c1) /\ (dom c2)
and E3: for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'xor' (Pj c2,b1) )
and E4: dom c4 = (dom c1) /\ (dom c2)
and E5: for b1 being set holds
( b1 in dom c4 implies Pj c4,b1 = (Pj c1,b1) 'xor' (Pj c2,b1) ) ;
for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = Pj c4,b1 )
proof
let c5 be set ;
assume c5 in dom c3 ;
then ( Pj c3,c5 = (Pj c1,c5) 'xor' (Pj c2,c5) & Pj c4,c5 = (Pj c1,c5) 'xor' (Pj c2,c5) ) by E2, E3, E4, E5;
hence Pj c3,c5 = Pj c4,c5 ;
end;
hence c3 = c4 by E2, E4, FUNCT_1:9;
end;
commutativity
for b1 being Function
for b2, b3 being boolean-valued Function holds
( ( dom b1 = (dom b2) /\ (dom b3) & for b4 being set holds
( b4 in dom b1 implies Pj b1,b4 = (Pj b2,b4) 'xor' (Pj b3,b4) ) ) implies ( ( dom b1 = (dom b3) /\ (dom b2) & for b4 being set holds
( b4 in dom b1 implies Pj b1,b4 = (Pj b3,b4) 'xor' (Pj b2,b4) ) ) ) ) ;
end;

:: deftheorem E2 defines 'or' BVFUNC_1:def 5 :
for b1, b2 being boolean-valued Function
for b3 being Function holds
( b3 = b1 'or' b2 iff ( dom b3 = (dom b1) /\ (dom b2) & for b4 being set holds
( b4 in dom b3 implies Pj b3,b4 = (Pj b1,b4) 'or' (Pj b2,b4) ) ) );

:: deftheorem E3 defines 'xor' BVFUNC_1:def 6 :
for b1, b2 being boolean-valued Function
for b3 being Function holds
( b3 = b1 'xor' b2 iff ( dom b3 = (dom b1) /\ (dom b2) & for b4 being set holds
( b4 in dom b3 implies Pj b3,b4 = (Pj b1,b4) 'xor' (Pj b2,b4) ) ) );

registration
let c1, c2 be boolean-valued Function;
cluster a1 'or' a2 -> boolean-valued ;
coherence
c1 'or' c2 is boolean-valued
proof
let c3 be set ; :: uses TARSKI:def 3,VALUAT_1:def 2
assume c3 in rng (c1 'or' c2) ;
then consider c4 being set such that
E4: c4 in dom (c1 'or' c2)
and E5: c3 = Pj (c1 'or' c2),c4 by FUNCT_1:def 5;
c3 = (Pj c1,c4) 'or' (Pj c2,c4) by E4, E5, E2;
then ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
hence c3 in BOOLEAN ;
end;
cluster a1 'xor' a2 -> boolean-valued ;
coherence
c1 'xor' c2 is boolean-valued
proof
let c3 be set ; :: uses TARSKI:def 3,VALUAT_1:def 2
assume c3 in rng (c1 'xor' c2) ;
then consider c4 being set such that
E4: c4 in dom (c1 'xor' c2)
and E5: c3 = Pj (c1 'xor' c2),c4 by FUNCT_1:def 5;
c3 = (Pj c1,c4) 'xor' (Pj c2,c4) by E4, E5, E3;
then ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
hence c3 in BOOLEAN ;
end;
end;

definition
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
redefine func 'or' as a2 'or' a3 -> Element of Funcs a1,BOOLEAN means :E4: :: BVFUNC_1:def 7
for b1 being Element of a1 holds a4 . b1 = (a2 . b1) 'or' (a3 . b1);
coherence
c2 'or' c3 is Element of Funcs c1,BOOLEAN
proof
E4: ex b1 being Function st
( c2 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
ex b1 being Function st
( c3 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
then E5: dom (c2 'or' c3) = c1 /\ c1 by E4, E2
.= c1 ;
rng (c2 'or' c3) c= BOOLEAN by VALUAT_1:def 2;
hence c2 'or' c3 is Element of Funcs c1,BOOLEAN by E5, FUNCT_2:def 2;
end;
compatibility
for b1 being Element of Funcs c1,BOOLEAN holds
( b1 = c2 'or' c3 iff for b2 being Element of c1 holds b1 . b2 = (c2 . b2) 'or' (c3 . b2) )
proof
let c4 be Element of Funcs c1,BOOLEAN ;
hereby
assume E4: c4 = c2 'or' c3 ;
let c5 be Element of c1;
E5: dom c2 = c1 by FUNCT_2:def 1;
dom c3 = c1 by FUNCT_2:def 1;
then dom (c2 'or' c3) = c1 /\ c1 by E5, E2
.= c1 ;
hence c4 . c5 = (c2 . c5) 'or' (c3 . c5) by E4, E2;
end; assume E4: for b1 being Element of c1 holds c4 . b1 = (c2 . b1) 'or' (c3 . b1) ;
E5: dom c4 = c1 by FUNCT_2:def 1;
E6: dom c3 = c1 by FUNCT_2:def 1;
E7: dom c4 = c1 /\ c1 by FUNCT_2:def 1
.= (dom c2) /\ (dom c3) by E6, FUNCT_2:def 1 ;
for b1 being set holds
( b1 in dom c4 implies Pj c4,b1 = (Pj c2,b1) 'or' (Pj c3,b1) ) by E4, E5;
hence c4 = c2 'or' c3 by E7, E2;
end;
redefine func 'xor' as a2 'xor' a3 -> Element of Funcs a1,BOOLEAN means :: BVFUNC_1:def 8
for b1 being Element of a1 holds a4 . b1 = (a2 . b1) 'xor' (a3 . b1);
coherence
c2 'xor' c3 is Element of Funcs c1,BOOLEAN
proof
E4: ex b1 being Function st
( c2 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
ex b1 being Function st
( c3 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
then E5: dom (c2 'xor' c3) = c1 /\ c1 by E4, E3
.= c1 ;
rng (c2 'xor' c3) c= BOOLEAN by VALUAT_1:def 2;
hence c2 'xor' c3 is Element of Funcs c1,BOOLEAN by E5, FUNCT_2:def 2;
end;
compatibility
for b1 being Element of Funcs c1,BOOLEAN holds
( b1 = c2 'xor' c3 iff for b2 being Element of c1 holds b1 . b2 = (c2 . b2) 'xor' (c3 . b2) )
proof
let c4 be Element of Funcs c1,BOOLEAN ;
hereby
assume E4: c4 = c2 'xor' c3 ;
let c5 be Element of c1;
E5: dom c2 = c1 by FUNCT_2:def 1;
dom c3 = c1 by FUNCT_2:def 1;
then dom (c2 'xor' c3) = c1 /\ c1 by E5, E3
.= c1 ;
hence c4 . c5 = (c2 . c5) 'xor' (c3 . c5) by E4, E3;
end; assume E4: for b1 being Element of c1 holds c4 . b1 = (c2 . b1) 'xor' (c3 . b1) ;
E5: dom c4 = c1 by FUNCT_2:def 1;
E6: dom c3 = c1 by FUNCT_2:def 1;
E7: dom c4 = c1 /\ c1 by FUNCT_2:def 1
.= (dom c2) /\ (dom c3) by E6, FUNCT_2:def 1 ;
for b1 being set holds
( b1 in dom c4 implies Pj c4,b1 = (Pj c2,b1) 'xor' (Pj c3,b1) ) by E4, E5;
hence c4 = c2 'xor' c3 by E7, E3;
end;
end;

:: deftheorem E4 defines 'or' BVFUNC_1:def 7 :
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b4 = b2 'or' b3 iff for b5 being Element of b1 holds b4 . b5 = (b2 . b5) 'or' (b3 . b5) );

:: deftheorem defines 'xor' BVFUNC_1:def 8 :
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b4 = b2 'xor' b3 iff for b5 being Element of b1 holds b4 . b5 = (b2 . b5) 'xor' (b3 . b5) );

definition
let c1 be non empty set ;
let c2, c3 be Element of BVF c1;
redefine func 'or' as a2 'or' a3 -> Element of BVF a1;
coherence
c2 'or' c3 is Element of BVF c1
proof
reconsider c4 = c2, c5 = c3 as Element of Funcs c1,BOOLEAN ;
c4 'or' c5 is Element of Funcs c1,BOOLEAN ;
hence c2 'or' c3 is Element of BVF c1 ;
end;
redefine func 'xor' as a2 'xor' a3 -> Element of BVF a1;
coherence
c2 'xor' c3 is Element of BVF c1
proof
reconsider c4 = c2, c5 = c3 as Element of Funcs c1,BOOLEAN ;
c4 'xor' c5 is Element of Funcs c1,BOOLEAN ;
hence c2 'xor' c3 is Element of BVF c1 ;
end;
end;

definition
let c1, c2 be boolean-valued Function;
func a1 'imp' a2 -> Function means :E5: :: BVFUNC_1:def 9
( dom a3 = (dom a1) /\ (dom a2) & for b1 being set holds
( b1 in dom a3 implies Pj a3,b1 = (Pj a1,b1) 'imp' (Pj a2,b1) ) );
existence
ex b1 being Function st
( dom b1 = (dom c1) /\ (dom c2) & for b2 being set holds
( b2 in dom b1 implies Pj b1,b2 = (Pj c1,b2) 'imp' (Pj c2,b2) ) )
proof
deffunc H1( set ) -> set = (Pj c1,a1) 'imp' (Pj c2,a1);
consider c3 being Function such that
E5: dom c3 = (dom c1) /\ (dom c2)
and E6: for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies Pj c3,b1 = H1(b1) ) from FUNCT_1:sch 3();
 take c3 ;
thus ( dom c3 = (dom c1) /\ (dom c2) & for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'imp' (Pj c2,b1) ) ) by E5, E6;
end;
uniqueness
for b1, b2 being Function holds
( ( dom b1 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b1 implies Pj b1,b3 = (Pj c1,b3) 'imp' (Pj c2,b3) ) & dom b2 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b2 implies Pj b2,b3 = (Pj c1,b3) 'imp' (Pj c2,b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Function;
assume that E5: dom c3 = (dom c1) /\ (dom c2)
and E6: for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'imp' (Pj c2,b1) )
and E7: dom c4 = (dom c1) /\ (dom c2)
and E8: for b1 being set holds
( b1 in dom c4 implies Pj c4,b1 = (Pj c1,b1) 'imp' (Pj c2,b1) ) ;
for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = Pj c4,b1 )
proof
let c5 be set ;
assume c5 in dom c3 ;
then ( Pj c3,c5 = (Pj c1,c5) 'imp' (Pj c2,c5) & Pj c4,c5 = (Pj c1,c5) 'imp' (Pj c2,c5) ) by E5, E6, E7, E8;
hence Pj c3,c5 = Pj c4,c5 ;
end;
hence c3 = c4 by E5, E7, FUNCT_1:9;
end;
func a1 'eqv' a2 -> Function means :E6: :: BVFUNC_1:def 10
( dom a3 = (dom a1) /\ (dom a2) & for b1 being set holds
( b1 in dom a3 implies Pj a3,b1 = (Pj a1,b1) 'eqv' (Pj a2,b1) ) );
existence
ex b1 being Function st
( dom b1 = (dom c1) /\ (dom c2) & for b2 being set holds
( b2 in dom b1 implies Pj b1,b2 = (Pj c1,b2) 'eqv' (Pj c2,b2) ) )
proof
deffunc H1( set ) -> set = (Pj c1,a1) 'eqv' (Pj c2,a1);
consider c3 being Function such that
E5: dom c3 = (dom c1) /\ (dom c2)
and E6: for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies Pj c3,b1 = H1(b1) ) from FUNCT_1:sch 3();
 take c3 ;
thus ( dom c3 = (dom c1) /\ (dom c2) & for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'eqv' (Pj c2,b1) ) ) by E5, E6;
end;
uniqueness
for b1, b2 being Function holds
( ( dom b1 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b1 implies Pj b1,b3 = (Pj c1,b3) 'eqv' (Pj c2,b3) ) & dom b2 = (dom c1) /\ (dom c2) & for b3 being set holds
( b3 in dom b2 implies Pj b2,b3 = (Pj c1,b3) 'eqv' (Pj c2,b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Function;
assume that E5: dom c3 = (dom c1) /\ (dom c2)
and E6: for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = (Pj c1,b1) 'eqv' (Pj c2,b1) )
and E7: dom c4 = (dom c1) /\ (dom c2)
and E8: for b1 being set holds
( b1 in dom c4 implies Pj c4,b1 = (Pj c1,b1) 'eqv' (Pj c2,b1) ) ;
for b1 being set holds
( b1 in dom c3 implies Pj c3,b1 = Pj c4,b1 )
proof
let c5 be set ;
assume c5 in dom c3 ;
then ( Pj c3,c5 = (Pj c1,c5) 'eqv' (Pj c2,c5) & Pj c4,c5 = (Pj c1,c5) 'eqv' (Pj c2,c5) ) by E5, E6, E7, E8;
hence Pj c3,c5 = Pj c4,c5 ;
end;
hence c3 = c4 by E5, E7, FUNCT_1:9;
end;
commutativity
for b1 being Function
for b2, b3 being boolean-valued Function holds
( ( dom b1 = (dom b2) /\ (dom b3) & for b4 being set holds
( b4 in dom b1 implies Pj b1,b4 = (Pj b2,b4) 'eqv' (Pj b3,b4) ) ) implies ( ( dom b1 = (dom b3) /\ (dom b2) & for b4 being set holds
( b4 in dom b1 implies Pj b1,b4 = (Pj b3,b4) 'eqv' (Pj b2,b4) ) ) ) ) ;
end;

:: deftheorem E5 defines 'imp' BVFUNC_1:def 9 :
for b1, b2 being boolean-valued Function
for b3 being Function holds
( b3 = b1 'imp' b2 iff ( dom b3 = (dom b1) /\ (dom b2) & for b4 being set holds
( b4 in dom b3 implies Pj b3,b4 = (Pj b1,b4) 'imp' (Pj b2,b4) ) ) );

:: deftheorem E6 defines 'eqv' BVFUNC_1:def 10 :
for b1, b2 being boolean-valued Function
for b3 being Function holds
( b3 = b1 'eqv' b2 iff ( dom b3 = (dom b1) /\ (dom b2) & for b4 being set holds
( b4 in dom b3 implies Pj b3,b4 = (Pj b1,b4) 'eqv' (Pj b2,b4) ) ) );

registration
let c1, c2 be boolean-valued Function;
cluster a1 'imp' a2 -> boolean-valued ;
coherence
c1 'imp' c2 is boolean-valued
proof
let c3 be set ; :: uses TARSKI:def 3,VALUAT_1:def 2
assume c3 in rng (c1 'imp' c2) ;
then consider c4 being set such that
E7: c4 in dom (c1 'imp' c2)
and E8: c3 = Pj (c1 'imp' c2),c4 by FUNCT_1:def 5;
c3 = (Pj c1,c4) 'imp' (Pj c2,c4) by E7, E8, E5
.= ('not' (Pj c1,c4)) 'or' (Pj c2,c4) ;
then ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
hence c3 in BOOLEAN ;
end;
cluster a1 'eqv' a2 -> boolean-valued ;
coherence
c1 'eqv' c2 is boolean-valued
proof
let c3 be set ; :: uses TARSKI:def 3,VALUAT_1:def 2
assume c3 in rng (c1 'eqv' c2) ;
then consider c4 being set such that
E7: c4 in dom (c1 'eqv' c2)
and E8: c3 = Pj (c1 'eqv' c2),c4 by FUNCT_1:def 5;
c3 = (Pj c1,c4) 'eqv' (Pj c2,c4) by E7, E8, E6
.= 'not' ((Pj c1,c4) 'xor' (Pj c2,c4)) ;
then ( c3 = FALSE or c3 = TRUE ) by MARGREL1:39;
hence c3 in BOOLEAN ;
end;
end;

definition
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
redefine func 'imp' as a2 'imp' a3 -> Element of Funcs a1,BOOLEAN means :E7: :: BVFUNC_1:def 11
for b1 being Element of a1 holds a4 . b1 = ('not' (Pj a2,b1)) 'or' (Pj a3,b1);
coherence
c2 'imp' c3 is Element of Funcs c1,BOOLEAN
proof
E7: ex b1 being Function st
( c2 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
ex b1 being Function st
( c3 = b1 & dom b1 = c1 & rng b1 c= BOOLEAN ) by FUNCT_2:def 2;
then E8: dom (c2 'imp' c3) = c1 /\ c1 by E7, E5
.= c1 ;
rng (c2 'imp' c3) c= BOOLEAN by VALUAT_1:def 2;
hence c2 'imp' c3 is Element of Funcs c1,BOOLEAN by E8, FUNCT_2:def 2;
end;
compatibility
for b1 being Element of Funcs c1,BOOLEAN holds
( b1 = c2 'imp' c3 iff for b2 being Element of c1 holds b1 . b2 = ('not' (Pj c2,b2)) 'or' (Pj c3,b2) )
proof
let c4 be Element of Funcs c1,BOOLEAN ;
hereby
assume E7: c4 = c2 'imp' c3 ;
let c5 be Element of c1;
E8: dom c2 = c1 by FUNCT_2:def 1;
dom c3 = c1 by FUNCT_2:def 1;
then dom (c2 'imp' c3) = c1 /\ c1 by E8, E5
.= c1 ;
hence c4 . c5 = (c2 . c5) 'imp' (c3 . c5) by E7, E5
.= ('not' (Pj c2,c5)) 'or' (Pj c3,c5) ;

end; assume E7: for b1 being Element of c1 holds c4 . b1 = ('not' (Pj c2,b1