let B be non empty non void bool-correct BoolSignature ; :: thesis: for A1 being non-empty bool-correct MSAlgebra over B
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
(B,A1) +* A2 is bool-correct
let A1 be non-empty bool-correct MSAlgebra over B; :: thesis: for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
(B,A1) +* A2 is bool-correct
let C be non empty non void ConnectivesSignature ; :: thesis: ( the carrier' of B misses the carrier' of C implies for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
(B,A1) +* A2 is bool-correct )
assume A1: the carrier' of B misses the carrier' of C ; :: thesis: for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
(B,A1) +* A2 is bool-correct
let A2 be non-empty MSAlgebra over C; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies (B,A1) +* A2 is bool-correct )
assume A2: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: (B,A1) +* A2 is bool-correct
set S = B +* C;
set A = (B,A1) +* A2;
A3: ( the Sorts of A1 . the bool-sort of B = BOOLEAN & (Den ((In (( the connectives of B . 1), the carrier' of B)),A1)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of B . 2), the carrier' of B)),A1)) . <*x*> = 'not' x & (Den ((In (( the connectives of B . 3), the carrier' of B)),A1)) . <*x,y*> = x '&' y ) ) ) by Def31;
A4: dom the Sorts of A1 = the carrier of B by PARTFUN1:def 2;
A5: ( the Sorts of ((B,A1) +* A2) = the Sorts of A1 +* the Sorts of A2 & the Charact of ((B,A1) +* A2) = the Charact of A1 +* the Charact of A2 ) by A2, CIRCCOMB:def 4;
the bool-sort of (B +* C) = the bool-sort of B by Def52;
hence the Sorts of ((B,A1) +* A2) . the bool-sort of (B +* C) = BOOLEAN by A2, A3, A4, A5, FUNCT_4:15; :: according to AOFA_A00:def 31 :: thesis: ( (Den ((In (( the connectives of (B +* C) . 1), the carrier' of (B +* C))),((B,A1) +* A2))) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of (B +* C) . 2), the carrier' of (B +* C))),((B,A1) +* A2))) . <*x*> = 'not' x & (Den ((In (( the connectives of (B +* C) . 3), the carrier' of (B +* C))),((B,A1) +* A2))) . <*x,y*> = x '&' y ) ) )
A6: the connectives of (B +* C) = the connectives of B ^ the connectives of C by Def52;
A7: len the connectives of B >= 3 by Def30;
then ( len the connectives of B >= 2 & len the connectives of B >= 1 ) by XXREAL_0:2;
then A8: ( 1 in dom the connectives of B & 2 in dom the connectives of B & 3 in dom the connectives of B ) by A7, FINSEQ_3:25;
A9: dom the connectives of B c= dom the connectives of (B +* C) by A6, FINSEQ_1:26;
A10: ( dom the Charact of A1 = the carrier' of B & dom the Charact of A2 = the carrier' of C ) by PARTFUN1:def 2;
A11: ( the connectives of (B +* C) . 1 in the carrier' of (B +* C) & the connectives of (B +* C) . 2 in the carrier' of (B +* C) & the connectives of (B +* C) . 3 in the carrier' of (B +* C) & the connectives of B . 1 in the carrier' of B & the connectives of B . 2 in the carrier' of B & the connectives of B . 3 in the carrier' of B ) by A9, A8, FUNCT_1:102;
( the connectives of (B +* C) . 1 = the connectives of B . 1 & the connectives of (B +* C) . 2 = the connectives of B . 2 & the connectives of (B +* C) . 3 = the connectives of B . 3 ) by A6, A8, FINSEQ_1:def 7;
then ( the connectives of (B +* C) . 1 = In (( the connectives of B . 1), the carrier' of B) & the connectives of (B +* C) . 2 = In (( the connectives of B . 2), the carrier' of B) & the connectives of (B +* C) . 3 = In (( the connectives of B . 3), the carrier' of B) ) by A8, FUNCT_1:102, SUBSET_1:def 8;
then ( In (( the connectives of (B +* C) . 1), the carrier' of (B +* C)) = In (( the connectives of B . 1), the carrier' of B) & In (( the connectives of (B +* C) . 2), the carrier' of (B +* C)) = In (( the connectives of B . 2), the carrier' of B) & In (( the connectives of (B +* C) . 3), the carrier' of (B +* C)) = In (( the connectives of B . 3), the carrier' of B) ) by A11, SUBSET_1:def 8;
then ( Den ((In (( the connectives of (B +* C) . 1), the carrier' of (B +* C))),((B,A1) +* A2)) = Den ((In (( the connectives of B . 1), the carrier' of B)),A1) & Den ((In (( the connectives of (B +* C) . 2), the carrier' of (B +* C))),((B,A1) +* A2)) = Den ((In (( the connectives of B . 2), the carrier' of B)),A1) & Den ((In (( the connectives of (B +* C) . 3), the carrier' of (B +* C))),((B,A1) +* A2)) = Den ((In (( the connectives of B . 3), the carrier' of B)),A1) ) by A1, A5, A10, FUNCT_4:16;
hence ( (Den ((In (( the connectives of (B +* C) . 1), the carrier' of (B +* C))),((B,A1) +* A2))) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of (B +* C) . 2), the carrier' of (B +* C))),((B,A1) +* A2))) . <*x*> = 'not' x & (Den ((In (( the connectives of (B +* C) . 3), the carrier' of (B +* C))),((B,A1) +* A2))) . <*x,y*> = x '&' y ) ) ) by Def31; :: thesis: verum