:: BVFUNC_7 semantic presentation

theorem Th1: :: BVFUNC_7:1
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) '&' (('not' b2) 'imp' b3) = b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . b1 = c3 . b1
proof
let c4 be Element of c1;
E2: ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = ((c2 'imp' c3) . c4) '&' ((('not' c2) 'imp' c3) . c4) by VALUAT_1:def 6
.= (('not' (c2 . c4)) 'or' (c3 . c4)) '&' ((('not' c2) 'imp' c3) . c4) by BVFUNC_1:def 11
.= (('not' (c2 . c4)) 'or' (c3 . c4)) '&' (('not' (('not' c2) . c4)) 'or' (c3 . c4)) by BVFUNC_1:def 11
.= (('not' (c2 . c4)) 'or' (c3 . c4)) '&' (('not' ('not' (c2 . c4))) 'or' (c3 . c4)) by VALUAT_1:def 5
.= (('not' (c2 . c4)) 'or' (c3 . c4)) '&' ((c2 . c4) 'or' (c3 . c4)) ;
now
per cases ( c2 . c4 = TRUE or c2 . c4 = FALSE ) by MARGREL1:39;
case c2 . c4 = TRUE ;
then ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = (FALSE 'or' (c3 . c4)) '&' (TRUE 'or' (c3 . c4)) by E2, MARGREL1:41
.= (FALSE 'or' (c3 . c4)) '&' TRUE by BINARITH:19
.= TRUE '&' (c3 . c4) by BINARITH:7
.= c3 . c4 by MARGREL1:50 ;
hence ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = c3 . c4 ;
end;
case c2 . c4 = FALSE ;
then ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = (TRUE 'or' (c3 . c4)) '&' (FALSE 'or' (c3 . c4)) by E2, MARGREL1:41
.= TRUE '&' (FALSE 'or' (c3 . c4)) by BINARITH:19
.= TRUE '&' (c3 . c4) by BINARITH:7
.= c3 . c4 by MARGREL1:50 ;
hence ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = c3 . c4 ;
end;
end;
end;
hence ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)) . c4 = c3 . c4 ;
end;
consider c4 being Function such that
E2: ( (c2 'imp' c3) '&' (('not' c2) 'imp' c3) = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E3: ( c3 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c4 & c1 = dom c5 & ( for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) ) ) by E1, E2, E3;
hence (c2 'imp' c3) '&' (('not' c2) 'imp' c3) = c3 by E2, E3, FUNCT_1:9;
end;

theorem Th2: :: BVFUNC_7:2
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) '&' (b2 'imp' ('not' b3)) = 'not' b2
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . b1 = ('not' c2) . b1
proof
let c4 be Element of c1;
E2: ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = ((c2 'imp' c3) . c4) '&' ((c2 'imp' ('not' c3)) . c4) by VALUAT_1:def 6
.= (('not' (c2 . c4)) 'or' (c3 . c4)) '&' ((c2 'imp' ('not' c3)) . c4) by BVFUNC_1:def 11
.= (('not' (c2 . c4)) 'or' (c3 . c4)) '&' (('not' (c2 . c4)) 'or' (('not' c3) . c4)) by BVFUNC_1:def 11
.= (('not' (c2 . c4)) 'or' (c3 . c4)) '&' (('not' (c2 . c4)) 'or' ('not' (c3 . c4))) by VALUAT_1:def 5 ;
now
per cases ( c3 . c4 = TRUE or c3 . c4 = FALSE ) by MARGREL1:39;
case c3 . c4 = TRUE ;
then ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = (('not' (c2 . c4)) 'or' TRUE ) '&' (('not' (c2 . c4)) 'or' FALSE ) by E2, MARGREL1:41
.= (('not' (c2 . c4)) 'or' TRUE ) '&' ('not' (c2 . c4)) by BINARITH:7
.= TRUE '&' ('not' (c2 . c4)) by BINARITH:19
.= 'not' (c2 . c4) by MARGREL1:50
.= ('not' c2) . c4 by VALUAT_1:def 5 ;
hence ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = ('not' c2) . c4 ;
end;
case c3 . c4 = FALSE ;
then ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = (('not' (c2 . c4)) 'or' FALSE ) '&' (('not' (c2 . c4)) 'or' TRUE ) by E2, MARGREL1:41
.= ('not' (c2 . c4)) '&' (('not' (c2 . c4)) 'or' TRUE ) by BINARITH:7
.= TRUE '&' ('not' (c2 . c4)) by BINARITH:19
.= 'not' (c2 . c4) by MARGREL1:50
.= ('not' c2) . c4 by VALUAT_1:def 5 ;
hence ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = ('not' c2) . c4 ;
end;
end;
end;
hence ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))) . c4 = ('not' c2) . c4 ;
end;
consider c4 being Function such that
E2: ( (c2 'imp' c3) '&' (c2 'imp' ('not' c3)) = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E3: ( 'not' c2 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c4 & c1 = dom c5 & ( for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) ) ) by E1, E2, E3;
hence (c2 'imp' c3) '&' (c2 'imp' ('not' c3)) = 'not' c2 by E2, E3, FUNCT_1:9;
end;

theorem Th3: :: BVFUNC_7:3
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'imp' (b3 'or' b4) = (b2 'imp' b3) 'or' (b2 'imp' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (c2 'imp' (c3 'or' c4)) . b1 = ((c2 'imp' c3) 'or' (c2 'imp' c4)) . b1
proof
let c5 be Element of c1;
((c2 'imp' c3) 'or' (c2 'imp' c4)) . c5 = ((c2 'imp' c3) . c5) 'or' ((c2 'imp' c4) . c5) by BVFUNC_1:def 7
.= (('not' (c2 . c5)) 'or' (c3 . c5)) 'or' ((c2 'imp' c4) . c5) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' (c3 . c5)) 'or' (('not' (c2 . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' (('not' (c2 . c5)) 'or' (c3 . c5))) 'or' (c4 . c5) by BINARITH:20
.= ((('not' (c2 . c5)) 'or' ('not' (c2 . c5))) 'or' (c3 . c5)) 'or' (c4 . c5) by BINARITH:20
.= (('not' (c2 . c5)) 'or' (c3 . c5)) 'or' (c4 . c5) by BINARITH:21
.= ('not' (c2 . c5)) 'or' ((c3 . c5) 'or' (c4 . c5)) by BINARITH:20
.= ('not' (c2 . c5)) 'or' ((c3 'or' c4) . c5) by BVFUNC_1:def 7
.= (c2 'imp' (c3 'or' c4)) . c5 by BVFUNC_1:def 11 ;
hence (c2 'imp' (c3 'or' c4)) . c5 = ((c2 'imp' c3) 'or' (c2 'imp' c4)) . c5 ;
end;
consider c5 being Function such that
E2: ( c2 'imp' (c3 'or' c4) = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
consider c6 being Function such that
E3: ( (c2 'imp' c3) 'or' (c2 'imp' c4) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c5 & c1 = dom c6 & ( for b1 being set holds
( b1 in c1 implies c5 . b1 = c6 . b1 ) ) ) by E1, E2, E3;
hence c2 'imp' (c3 'or' c4) = (c2 'imp' c3) 'or' (c2 'imp' c4) by E2, E3, FUNCT_1:9;
end;

theorem Th4: :: BVFUNC_7:4
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'imp' (b3 '&' b4) = (b2 'imp' b3) '&' (b2 'imp' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (c2 'imp' (c3 '&' c4)) . b1 = ((c2 'imp' c3) '&' (c2 'imp' c4)) . b1
proof
let c5 be Element of c1;
((c2 'imp' c3) '&' (c2 'imp' c4)) . c5 = ((c2 'imp' c3) . c5) '&' ((c2 'imp' c4) . c5) by VALUAT_1:def 6
.= (('not' (c2 . c5)) 'or' (c3 . c5)) '&' ((c2 'imp' c4) . c5) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' (c3 . c5)) '&' (('not' (c2 . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= ('not' (c2 . c5)) 'or' ((c3 . c5) '&' (c4 . c5)) by BINARITH:23
.= ('not' (c2 . c5)) 'or' ((c3 '&' c4) . c5) by VALUAT_1:def 6
.= (c2 'imp' (c3 '&' c4)) . c5 by BVFUNC_1:def 11 ;
hence (c2 'imp' (c3 '&' c4)) . c5 = ((c2 'imp' c3) '&' (c2 'imp' c4)) . c5 ;
end;
consider c5 being Function such that
E2: ( c2 'imp' (c3 '&' c4) = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
consider c6 being Function such that
E3: ( (c2 'imp' c3) '&' (c2 'imp' c4) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c5 & c1 = dom c6 & ( for b1 being set holds
( b1 in c1 implies c5 . b1 = c6 . b1 ) ) ) by E1, E2, E3;
hence c2 'imp' (c3 '&' c4) = (c2 'imp' c3) '&' (c2 'imp' c4) by E2, E3, FUNCT_1:9;
end;

theorem Th5: :: BVFUNC_7:5
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 'or' b3) 'imp' b4 = (b2 'imp' b4) '&' (b3 'imp' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds ((c2 'or' c3) 'imp' c4) . b1 = ((c2 'imp' c4) '&' (c3 'imp' c4)) . b1
proof
let c5 be Element of c1;
((c2 'imp' c4) '&' (c3 'imp' c4)) . c5 = ((c2 'imp' c4) . c5) '&' ((c3 'imp' c4) . c5) by VALUAT_1:def 6
.= (('not' (c2 . c5)) 'or' (c4 . c5)) '&' ((c3 'imp' c4) . c5) by BVFUNC_1:def 11
.= ((c4 . c5) 'or' ('not' (c2 . c5))) '&' (('not' (c3 . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= (c4 . c5) 'or' (('not' (c2 . c5)) '&' ('not' (c3 . c5))) by BINARITH:23
.= ('not' ((c2 . c5) 'or' (c3 . c5))) 'or' (c4 . c5) by BINARITH:10
.= ('not' ((c2 'or' c3) . c5)) 'or' (c4 . c5) by BVFUNC_1:def 7
.= ((c2 'or' c3) 'imp' c4) . c5 by BVFUNC_1:def 11 ;
hence ((c2 'or' c3) 'imp' c4) . c5 = ((c2 'imp' c4) '&' (c3 'imp' c4)) . c5 ;
end;
consider c5 being Function such that
E2: ( (c2 'or' c3) 'imp' c4 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
consider c6 being Function such that
E3: ( (c2 'imp' c4) '&' (c3 'imp' c4) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c5 & c1 = dom c6 & ( for b1 being set holds
( b1 in c1 implies c5 . b1 = c6 . b1 ) ) ) by E1, E2, E3;
hence (c2 'or' c3) 'imp' c4 = (c2 'imp' c4) '&' (c3 'imp' c4) by E2, E3, FUNCT_1:9;
end;

theorem Th6: :: BVFUNC_7:6
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 '&' b3) 'imp' b4 = (b2 'imp' b4) 'or' (b3 'imp' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds ((c2 '&' c3) 'imp' c4) . b1 = ((c2 'imp' c4) 'or' (c3 'imp' c4)) . b1
proof
let c5 be Element of c1;
((c2 'imp' c4) 'or' (c3 'imp' c4)) . c5 = ((c2 'imp' c4) . c5) 'or' ((c3 'imp' c4) . c5) by BVFUNC_1:def 7
.= (('not' (c2 . c5)) 'or' (c4 . c5)) 'or' ((c3 'imp' c4) . c5) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' (c4 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' ((c4 . c5) 'or' ('not' (c3 . c5)))) 'or' (c4 . c5) by BINARITH:20
.= ((('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5)) 'or' (c4 . c5) by BINARITH:20
.= (('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' ((c4 . c5) 'or' (c4 . c5)) by BINARITH:20
.= (('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5) by BINARITH:21
.= ('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5) by BINARITH:9
.= ('not' ((c2 '&' c3) . c5)) 'or' (c4 . c5) by VALUAT_1:def 6
.= ((c2 '&' c3) 'imp' c4) . c5 by BVFUNC_1:def 11 ;
hence ((c2 '&' c3) 'imp' c4) . c5 = ((c2 'imp' c4) 'or' (c3 'imp' c4)) . c5 ;
end;
consider c5 being Function such that
E2: ( (c2 '&' c3) 'imp' c4 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
consider c6 being Function such that
E3: ( (c2 'imp' c4) 'or' (c3 'imp' c4) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c5 & c1 = dom c6 & ( for b1 being set holds
( b1 in c1 implies c5 . b1 = c6 . b1 ) ) ) by E1, E2, E3;
hence (c2 '&' c3) 'imp' c4 = (c2 'imp' c4) 'or' (c3 'imp' c4) by E2, E3, FUNCT_1:9;
end;

theorem Th7: :: BVFUNC_7:7
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 '&' b3) 'imp' b4 = b2 'imp' (b3 'imp' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds ((c2 '&' c3) 'imp' c4) . b1 = (c2 'imp' (c3 'imp' c4)) . b1
proof
let c5 be Element of c1;
(c2 'imp' (c3 'imp' c4)) . c5 = ('not' (c2 . c5)) 'or' ((c3 'imp' c4) . c5) by BVFUNC_1:def 11
.= ('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= (('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5) by BINARITH:20
.= ('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5) by BINARITH:9
.= ('not' ((c2 '&' c3) . c5)) 'or' (c4 . c5) by VALUAT_1:def 6
.= ((c2 '&' c3) 'imp' c4) . c5 by BVFUNC_1:def 11 ;
hence ((c2 '&' c3) 'imp' c4) . c5 = (c2 'imp' (c3 'imp' c4)) . c5 ;
end;
consider c5 being Function such that
E3: ( (c2 '&' c3) 'imp' c4 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
consider c6 being Function such that
E4: ( c2 'imp' (c3 'imp' c4) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c5 & c1 = dom c6 & ( for b1 being set holds
( b1 in c1 implies c5 . b1 = c6 . b1 ) ) ) by E2, E3, E4;
hence (c2 '&' c3) 'imp' c4 = c2 'imp' (c3 'imp' c4) by E3, E4, FUNCT_1:9;
end;

theorem Th8: :: BVFUNC_7:8
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 '&' b3) 'imp' b4 = b2 'imp' (('not' b3) 'or' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds ((c2 '&' c3) 'imp' c4) . b1 = (c2 'imp' (('not' c3) 'or' c4)) . b1
proof
let c5 be Element of c1;
(c2 'imp' (('not' c3) 'or' c4)) . c5 = (c2 'imp' (c3 'imp' c4)) . c5 by BVFUNC_4:8;
hence ((c2 '&' c3) 'imp' c4) . c5 = (c2 'imp' (('not' c3) 'or' c4)) . c5 by Th7;
end;
consider c5 being Function such that
E3: ( (c2 '&' c3) 'imp' c4 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
consider c6 being Function such that
E4: ( c2 'imp' (('not' c3) 'or' c4) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c5 & c1 = dom c6 & ( for b1 being set holds
( b1 in c1 implies c5 . b1 = c6 . b1 ) ) ) by E2, E3, E4;
hence (c2 '&' c3) 'imp' c4 = c2 'imp' (('not' c3) 'or' c4) by E3, E4, FUNCT_1:9;
end;

theorem Th9: :: BVFUNC_7:9
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'imp' (b3 'or' b4) = (b2 '&' ('not' b3)) 'imp' b4
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds (c2 'imp' (c3 'or' c4)) . b1 = ((c2 '&' ('not' c3)) 'imp' c4) . b1
proof
let c5 be Element of c1;
((c2 '&' ('not' c3)) 'imp' c4) . c5 = ('not' ((c2 '&' ('not' c3)) . c5)) 'or' (c4 . c5) by BVFUNC_1:def 11
.= ('not' ((c2 . c5) '&' (('not' c3) . c5))) 'or' (c4 . c5) by VALUAT_1:def 6
.= (('not' (c2 . c5)) 'or' ('not' (('not' c3) . c5))) 'or' (c4 . c5) by BINARITH:9
.= (('not' (c2 . c5)) 'or' ('not' ('not' (c3 . c5)))) 'or' (c4 . c5) by VALUAT_1:def 5
.= (('not' (c2 . c5)) 'or' (c3 . c5)) 'or' (c4 . c5)
.= ('not' (c2 . c5)) 'or' ((c3 . c5) 'or' (c4 . c5)) by BINARITH:20
.= ('not' (c2 . c5)) 'or' ((c3 'or' c4) . c5) by BVFUNC_1:def 7
.= (c2 'imp' (c3 'or' c4)) . c5 by BVFUNC_1:def 11 ;
hence (c2 'imp' (c3 'or' c4)) . c5 = ((c2 '&' ('not' c3)) 'imp' c4) . c5 ;
end;
consider c5 being Function such that
E3: ( c2 'imp' (c3 'or' c4) = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
consider c6 being Function such that
E4: ( (c2 '&' ('not' c3)) 'imp' c4 = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c5 & c1 = dom c6 & ( for b1 being set holds
( b1 in c1 implies c5 . b1 = c6 . b1 ) ) ) by E2, E3, E4;
hence c2 'imp' (c3 'or' c4) = (c2 '&' ('not' c3)) 'imp' c4 by E3, E4, FUNCT_1:9;
end;

theorem Th10: :: BVFUNC_7:10
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 '&' (b2 'imp' b3) = b2 '&' b3
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds (c2 '&' (c2 'imp' c3)) . b1 = (c2 '&' c3) . b1
proof
let c4 be Element of c1;
(c2 '&' (c2 'imp' c3)) . c4 = (c2 . c4) '&' ((c2 'imp' c3) . c4) by VALUAT_1:def 6
.= (c2 . c4) '&' (('not' (c2 . c4)) 'or' (c3 . c4)) by BVFUNC_1:def 11
.= ((c2 . c4) '&' ('not' (c2 . c4))) 'or' ((c2 . c4) '&' (c3 . c4)) by BINARITH:22
.= FALSE 'or' ((c2 . c4) '&' (c3 . c4)) by MARGREL1:46
.= (c2 . c4) '&' (c3 . c4) by BINARITH:7
.= (c2 '&' c3) . c4 by VALUAT_1:def 6 ;
hence (c2 '&' (c2 'imp' c3)) . c4 = (c2 '&' c3) . c4 ;
end;
consider c4 being Function such that
E3: ( c2 '&' (c2 'imp' c3) = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
consider c5 being Function such that
E4: ( c2 '&' c3 = c5 & dom c5 = c1 & rng c5 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c4 & c1 = dom c5 & ( for b1 being set holds
( b1 in c1 implies c4 . b1 = c5 . b1 ) ) ) by E2, E3, E4;
hence c2 '&' (c2 'imp' c3) = c2 '&' c3 by E3, E4, FUNCT_1:9;
end;

theorem Th11: :: BVFUNC_7:11
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) '&' ('not' b3) = ('not' b2) '&' ('not' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds ((c2 'imp' c3) '&' ('not' c3)) . b1 = (('not' c2) '&' ('not' c3)) . b1
proof
let c4 be Element of c1;
((c2 'imp' c3) '&' ('not' c3)) . c4 = ((c2 'imp' c3) . c4) '&' (('not' c3) . c4) by VALUAT_1:def 6
.= (('not' c3) . c4) '&' (('not' (c2 . c4)) 'or' (c3 . c4)) by BVFUNC_1:def 11
.= ((('not' c3) . c4) '&' ('not' (c2 . c4))) 'or' ((('not' c3) . c4) '&' (c3 . c4)) by BINARITH:22
.= ((('not' c3) . c4) '&' ('not' (c2 . c4))) 'or' ((c3 . c4) '&' ('not' (c3 . c4))) by VALUAT_1:def 5
.= ((('not' c3) . c4) '&' ('not' (c2 . c4))) 'or' FALSE by MARGREL1:46
.= (('not' c3) . c4) '&' ('not' (c2 . c4)) by BINARITH:7
.= (('not' c3) . c4) '&' (('not' c2) . c4) by VALUAT_1:def 5
.= (('not' c2) '&' ('not' c3)) . c4 by VALUAT_1:def 6 ;
hence ((c2 'imp' c3) '&' ('not' c3)) . c4 = (('not' c2) '&' ('not' c3)) . c4 ;
end;
consider c4 being Function such that
E3: ( (c2 'imp' c3) '&' ('not' c