let B be non empty non void bool-correct BoolSignature ; 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; 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 ; ( 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
; 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; ( 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
; (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; AOFA_A00:def 31 ( (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; verum