let B be non empty non void bool-correct BoolSignature ; :: thesis: for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds

B +* C is bool-correct

let C be non empty non void ConnectivesSignature ; :: thesis: ( the carrier' of B misses the carrier' of C implies B +* C is bool-correct )

assume A1: the carrier' of B misses the carrier' of C ; :: thesis: B +* C is bool-correct

set S = B +* C;

A2: the connectives of (B +* C) = the connectives of B ^ the connectives of C by Def52;

then A3: len the connectives of (B +* C) = (len the connectives of B) + (len the connectives of C) by FINSEQ_1:22;

A4: len the connectives of B >= 3 by Def30;

hence len the connectives of (B +* C) >= 3 by A3, NAT_1:12; :: according to AOFA_A00:def 30 :: thesis: ( the connectives of (B +* C) . 1 is_of_type {} , the bool-sort of (B +* C) & the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) & the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) )

A13: 1 <= len the connectives of B by A4, XXREAL_0:2;

the connectives of B . 1 is_of_type {} , the bool-sort of B by Def30;

hence the connectives of (B +* C) . 1 is_of_type {} , the bool-sort of (B +* C) by A5, A12, A13; :: thesis: ( the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) & the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) )

A14: 2 <= len the connectives of B by A4, XXREAL_0:2;

the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B by Def30;

hence the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) by A5, A12, A14; :: thesis: the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C)

the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B by Def30;

hence the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) by A5, A4, A12; :: thesis: verum

B +* C is bool-correct

let C be non empty non void ConnectivesSignature ; :: thesis: ( the carrier' of B misses the carrier' of C implies B +* C is bool-correct )

assume A1: the carrier' of B misses the carrier' of C ; :: thesis: B +* C is bool-correct

set S = B +* C;

A2: the connectives of (B +* C) = the connectives of B ^ the connectives of C by Def52;

then A3: len the connectives of (B +* C) = (len the connectives of B) + (len the connectives of C) by FINSEQ_1:22;

A4: len the connectives of B >= 3 by Def30;

hence len the connectives of (B +* C) >= 3 by A3, NAT_1:12; :: according to AOFA_A00:def 30 :: thesis: ( the connectives of (B +* C) . 1 is_of_type {} , the bool-sort of (B +* C) & the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) & the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) )

A5: now :: thesis: for i being Nat st 1 <= i & i <= len the connectives of B holds

( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set

for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J ) )

A12:
the bool-sort of (B +* C) = the bool-sort of B
by Def52;( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set

for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J ) )

let i be Nat; :: thesis: ( 1 <= i & i <= len the connectives of B implies ( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set

for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J ) ) )

assume ( 1 <= i & i <= len the connectives of B ) ; :: thesis: ( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set

for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J ) )

then A6: i in dom the connectives of B by FINSEQ_3:25;

then the connectives of B . i in the carrier' of B by FUNCT_1:102;

then A7: the connectives of B . i nin the carrier' of C by A1, XBOOLE_0:3;

A8: ( dom the Arity of C = the carrier' of C & dom the ResultSort of C = the carrier' of C ) by FUNCT_2:def 1;

( the Arity of (B +* C) = the Arity of B +* the Arity of C & the ResultSort of (B +* C) = the ResultSort of B +* the ResultSort of C ) by Th51;

then A9: ( the Arity of (B +* C) . ( the connectives of B . i) = the Arity of B . ( the connectives of B . i) & the ResultSort of (B +* C) . ( the connectives of B . i) = the ResultSort of B . ( the connectives of B . i) ) by A7, A8, FUNCT_4:11;

thus A10: the connectives of (B +* C) . i = the connectives of B . i by A2, A6, FINSEQ_1:def 7; :: thesis: for x being set

for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J

let x be set ; :: thesis: for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J

let I be Element of B; :: thesis: for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J

let J be Element of (B +* C); :: thesis: ( I = J & the connectives of B . i is_of_type x,I implies the connectives of (B +* C) . i is_of_type x,J )

assume A11: ( I = J & the connectives of B . i is_of_type x,I ) ; :: thesis: the connectives of (B +* C) . i is_of_type x,J

thus the connectives of (B +* C) . i is_of_type x,J by A9, A11, A10; :: thesis: verum

end;for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J ) ) )

assume ( 1 <= i & i <= len the connectives of B ) ; :: thesis: ( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set

for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J ) )

then A6: i in dom the connectives of B by FINSEQ_3:25;

then the connectives of B . i in the carrier' of B by FUNCT_1:102;

then A7: the connectives of B . i nin the carrier' of C by A1, XBOOLE_0:3;

A8: ( dom the Arity of C = the carrier' of C & dom the ResultSort of C = the carrier' of C ) by FUNCT_2:def 1;

( the Arity of (B +* C) = the Arity of B +* the Arity of C & the ResultSort of (B +* C) = the ResultSort of B +* the ResultSort of C ) by Th51;

then A9: ( the Arity of (B +* C) . ( the connectives of B . i) = the Arity of B . ( the connectives of B . i) & the ResultSort of (B +* C) . ( the connectives of B . i) = the ResultSort of B . ( the connectives of B . i) ) by A7, A8, FUNCT_4:11;

thus A10: the connectives of (B +* C) . i = the connectives of B . i by A2, A6, FINSEQ_1:def 7; :: thesis: for x being set

for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J

let x be set ; :: thesis: for I being Element of B

for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J

let I be Element of B; :: thesis: for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds

the connectives of (B +* C) . i is_of_type x,J

let J be Element of (B +* C); :: thesis: ( I = J & the connectives of B . i is_of_type x,I implies the connectives of (B +* C) . i is_of_type x,J )

assume A11: ( I = J & the connectives of B . i is_of_type x,I ) ; :: thesis: the connectives of (B +* C) . i is_of_type x,J

thus the connectives of (B +* C) . i is_of_type x,J by A9, A11, A10; :: thesis: verum

A13: 1 <= len the connectives of B by A4, XXREAL_0:2;

the connectives of B . 1 is_of_type {} , the bool-sort of B by Def30;

hence the connectives of (B +* C) . 1 is_of_type {} , the bool-sort of (B +* C) by A5, A12, A13; :: thesis: ( the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) & the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) )

A14: 2 <= len the connectives of B by A4, XXREAL_0:2;

the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B by Def30;

hence the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) by A5, A12, A14; :: thesis: the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C)

the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B by Def30;

hence the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) by A5, A4, A12; :: thesis: verum