let S be non empty non void bool-correct BoolSignature ; :: thesis: for A being V2() ManySortedSet of the carrier of S ex B being strict non-empty MSAlgebra over S st
( the Sorts of B = A +* ( the bool-sort of S,BOOLEAN) & B is bool-correct )
let A be V2() ManySortedSet of the carrier of S; :: thesis: ex B being strict non-empty MSAlgebra over S st
( the Sorts of B = A +* ( the bool-sort of S,BOOLEAN) & B is bool-correct )
set A1 = A +* ( the bool-sort of S,BOOLEAN);
set Ch = the ManySortedFunction of ((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S,(A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S;
deffunc H₁( Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = $1 '&' $2;
consider f being non empty homogeneous quasi_total 2 -ary PartFunc of (BOOLEAN *),BOOLEAN such that
A1: for a, b being Element of BOOLEAN holds f . <*a,b*> = H₁(a,b) from AOFA_A00:sch 3();
deffunc H₂( Element of BOOLEAN ) -> Element of BOOLEAN = 'not' $1;
consider f1 being non empty homogeneous quasi_total 1 -ary PartFunc of (BOOLEAN *),BOOLEAN such that
A2: for a being Element of BOOLEAN holds f1 . <*a*> = H₂(a) from AOFA_A00:sch 2();
A3: dom f1 = (arity f1) -tuples_on BOOLEAN by COMPUT_1:22
.= 1 -tuples_on BOOLEAN by COMPUT_1:def 21 ;
A4: rng f1 c= BOOLEAN by RELAT_1:def 19;
A5: dom f = (arity f) -tuples_on BOOLEAN by COMPUT_1:22
.= 2 -tuples_on BOOLEAN by COMPUT_1:def 21 ;
A6: rng f c= BOOLEAN by RELAT_1:def 19;
A7: 3 <= len the connectives of S by Def30;
then ( 1 <= len the connectives of S & 2 <= len the connectives of S ) by XXREAL_0:2;
then A8: ( 1 in dom the connectives of S & 2 in dom the connectives of S & 3 in dom the connectives of S ) by A7, FINSEQ_3:25;
reconsider o1 = the connectives of S . 2, o2 = the connectives of S . 3, o0 = the connectives of S . 1 as OperSymbol of S by A8, DTCONSTR:2;
set Ch1 = ( the ManySortedFunction of ((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S,(A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S +* (o1,f1)) +* (o2,f);
set bs = the bool-sort of S;
A9: <* the bool-sort of S*> in the carrier of S * by FINSEQ_1:def 11;
A10: ( dom A = the carrier of S & dom (A +* ( the bool-sort of S,BOOLEAN)) = the carrier of S ) by PARTFUN1:def 2;
then A11: (A +* ( the bool-sort of S,BOOLEAN)) . the bool-sort of S = BOOLEAN by FUNCT_7:31;
o1 is_of_type <* the bool-sort of S*>, the bool-sort of S by Def30;
then A12: ( the_arity_of o1 = <* the bool-sort of S*> & the_result_sort_of o1 = the bool-sort of S ) ;
then A13: (((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S) . o1 = ((A +* ( the bool-sort of S,BOOLEAN)) #) . <* the bool-sort of S*> by FUNCT_2:15
.= product ((A +* ( the bool-sort of S,BOOLEAN)) * <* the bool-sort of S*>) by A9, FINSEQ_2:def 5
.= product <*((A +* ( the bool-sort of S,BOOLEAN)) . the bool-sort of S)*> by A10, FINSEQ_2:34
.= 1 -tuples_on BOOLEAN by A11, FINSEQ_3:126 ;
((A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S) . o1 = (A +* ( the bool-sort of S,BOOLEAN)) . the bool-sort of S by A12, FUNCT_2:15;
then f1 is Function of ((((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S) . o1),(((A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S) . o1) by A13, A11, A3, A4, FUNCT_2:2;
then reconsider Ch2 = the ManySortedFunction of ((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S,(A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S +* (o1,f1) as ManySortedFunction of ((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S,(A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S by Th45;
A14: <* the bool-sort of S, the bool-sort of S*> in the carrier of S * by FINSEQ_1:def 11;
o2 is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S by Def30;
then A15: ( the_arity_of o2 = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o2 = the bool-sort of S ) ;
then A16: (((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S) . o2 = ((A +* ( the bool-sort of S,BOOLEAN)) #) . <* the bool-sort of S, the bool-sort of S*> by FUNCT_2:15
.= product ((A +* ( the bool-sort of S,BOOLEAN)) * <* the bool-sort of S, the bool-sort of S*>) by A14, FINSEQ_2:def 5
.= product <*((A +* ( the bool-sort of S,BOOLEAN)) . the bool-sort of S),((A +* ( the bool-sort of S,BOOLEAN)) . the bool-sort of S)*> by A10, FINSEQ_2:125
.= 2 -tuples_on BOOLEAN by A11, FINSEQ_3:128 ;
((A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S) . o2 = (A +* ( the bool-sort of S,BOOLEAN)) . the bool-sort of S by A15, FUNCT_2:15;
then f is Function of ((((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S) . o2),(((A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S) . o2) by A16, A11, A5, A6, FUNCT_2:2;
then reconsider Ch1 = Ch2 +* (o2,f) as ManySortedFunction of ((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S,(A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S by Th45;
reconsider t = TRUE as Element of BOOLEAN ;
set f0 = (0 -tuples_on BOOLEAN) --> t;
( dom ((0 -tuples_on BOOLEAN) --> t) = 0 -tuples_on BOOLEAN & rng ((0 -tuples_on BOOLEAN) --> t) c= {t} & {t} c= BOOLEAN ) by ZFMISC_1:31;
then reconsider f0 = (0 -tuples_on BOOLEAN) --> t as Function of (0 -tuples_on BOOLEAN),BOOLEAN by FUNCT_2:2;
A17: <*> the carrier of S in the carrier of S * by FINSEQ_1:def 11;
o0 is_of_type {} , the bool-sort of S by Def30;
then A18: ( the_arity_of o0 = {} & the_result_sort_of o0 = the bool-sort of S ) ;
then A19: (((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S) . o0 = ((A +* ( the bool-sort of S,BOOLEAN)) #) . {} by FUNCT_2:15
.= product ((A +* ( the bool-sort of S,BOOLEAN)) * {}) by A17, FINSEQ_2:def 5
.= product (<*> BOOLEAN)
.= 0 -tuples_on BOOLEAN by FINSEQ_2:94, CARD_3:10 ;
((A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S) . o0 = (A +* ( the bool-sort of S,BOOLEAN)) . the bool-sort of S by A18, FUNCT_2:15;
then reconsider Ch3 = Ch1 +* (o0,f0) as ManySortedFunction of ((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S,(A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S by A19, A11, Th45;
set B = MSAlgebra(# (A +* ( the bool-sort of S,BOOLEAN)),Ch3 #);
MSAlgebra(# (A +* ( the bool-sort of S,BOOLEAN)),Ch3 #) is non-empty ;
then reconsider B = MSAlgebra(# (A +* ( the bool-sort of S,BOOLEAN)),Ch3 #) as strict non-empty MSAlgebra over S ;
take B ; :: thesis: ( the Sorts of B = A +* ( the bool-sort of S,BOOLEAN) & B is bool-correct )
thus the Sorts of B = A +* ( the bool-sort of S,BOOLEAN) ; :: thesis: B is bool-correct
thus the Sorts of B . the bool-sort of S = BOOLEAN by A10, FUNCT_7:31; :: according to AOFA_A00:def 31 :: thesis: ( (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> = x '&' y ) ) )
A20: ( len (the_arity_of o0) = 0 & len (the_arity_of o1) = 1 & len (the_arity_of o2) = 2 ) by A12, A15, A18, FINSEQ_1:40, FINSEQ_1:44;
A21: ( dom Ch2 = the carrier' of S & dom the ManySortedFunction of ((A +* ( the bool-sort of S,BOOLEAN)) #) * the Arity of S,(A +* ( the bool-sort of S,BOOLEAN)) * the ResultSort of S = the carrier' of S & dom Ch1 = the carrier' of S ) by PARTFUN1:def 2;
A22: Ch3 . o1 = Ch1 . o1 by A12, A18, FUNCT_7:32
.= Ch2 . o1 by A20, FUNCT_7:32
.= f1 by A21, FUNCT_7:31 ;
A23: Ch3 . o0 = f0 by A21, FUNCT_7:31;
( In (( the connectives of S . 1), the carrier' of S) = o0 & {} in {{}} & 0 -tuples_on BOOLEAN = {(<*> BOOLEAN)} ) by TARSKI:def 1, FINSEQ_2:94;
hence (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE by A23, FUNCOP_1:7; :: thesis: for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> = x '&' y )