let m be Nat; :: thesis: ( m > 0 implies for s being set
for B being non empty non void BoolSignature
for C being non empty non void ConnectivesSignature st B is m,s integer & the carrier' of B misses the carrier' of C holds
B +* C is m,s integer )
assume A1: m > 0 ; :: thesis: for s being set
for B being non empty non void BoolSignature
for C being non empty non void ConnectivesSignature st B is m,s integer & the carrier' of B misses the carrier' of C holds
B +* C is m,s integer
let s be set ; :: thesis: for B being non empty non void BoolSignature
for C being non empty non void ConnectivesSignature st B is m,s integer & the carrier' of B misses the carrier' of C holds
B +* C is m,s integer
let B be non empty non void BoolSignature ; :: thesis: for C being non empty non void ConnectivesSignature st B is m,s integer & the carrier' of B misses the carrier' of C holds
B +* C is m,s integer
let C be non empty non void ConnectivesSignature ; :: thesis: ( B is m,s integer & the carrier' of B misses the carrier' of C implies B +* C is m,s integer )
assume A2: len the connectives of B >= m + 6 ; :: according to AOFA_A00:def 38 :: thesis: ( for I being Element of B holds
( not I = s or not I <> the bool-sort of B or not the connectives of B . m is_of_type {} ,I or not the connectives of B . (m + 1) is_of_type {} ,I or not the connectives of B . m <> the connectives of B . (m + 1) or not the connectives of B . (m + 2) is_of_type <*I*>,I or not the connectives of B . (m + 3) is_of_type <*I,I*>,I or not the connectives of B . (m + 4) is_of_type <*I,I*>,I or not the connectives of B . (m + 5) is_of_type <*I,I*>,I or not the connectives of B . (m + 3) <> the connectives of B . (m + 4) or not the connectives of B . (m + 3) <> the connectives of B . (m + 5) or not the connectives of B . (m + 4) <> the connectives of B . (m + 5) or not the connectives of B . (m + 6) is_of_type <*I,I*>, the bool-sort of B ) or not the carrier' of B misses the carrier' of C or B +* C is m,s integer )
given I being Element of B such that A3: ( I = s & I <> the bool-sort of B & the connectives of B . m is_of_type {} ,I & the connectives of B . (m + 1) is_of_type {} ,I & the connectives of B . m <> the connectives of B . (m + 1) & the connectives of B . (m + 2) is_of_type <*I*>,I & the connectives of B . (m + 3) is_of_type <*I,I*>,I & the connectives of B . (m + 4) is_of_type <*I,I*>,I & the connectives of B . (m + 5) is_of_type <*I,I*>,I & the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) & the connectives of B . (m + 6) is_of_type <*I,I*>, the bool-sort of B ) ; :: thesis: ( not the carrier' of B misses the carrier' of C or B +* C is m,s integer )
assume A4: the carrier' of B misses the carrier' of C ; :: thesis: B +* C is m,s integer
set S = B +* C;
A5: the connectives of (B +* C) = the connectives of B ^ the connectives of C by Def52;
then len the connectives of (B +* C) = (len the connectives of B) + (len the connectives of C) by FINSEQ_1:22;
hence len the connectives of (B +* C) >= m + 6 by A2, NAT_1:12; :: according to AOFA_A00:def 38 :: thesis: ex I being Element of (B +* C) st
( I = s & I <> the bool-sort of (B +* C) & the connectives of (B +* C) . m is_of_type {} ,I & the connectives of (B +* C) . (m + 1) is_of_type {} ,I & the connectives of (B +* C) . m <> the connectives of (B +* C) . (m + 1) & the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I & the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
the carrier of (B +* C) = the carrier of B \/ the carrier of C by Th51;
then reconsider I = I as Element of (B +* C) by XBOOLE_0:def 3;
take I ; :: thesis: ( I = s & I <> the bool-sort of (B +* C) & the connectives of (B +* C) . m is_of_type {} ,I & the connectives of (B +* C) . (m + 1) is_of_type {} ,I & the connectives of (B +* C) . m <> the connectives of (B +* C) . (m + 1) & the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I & the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
thus I = s by A3; :: thesis: ( I <> the bool-sort of (B +* C) & the connectives of (B +* C) . m is_of_type {} ,I & the connectives of (B +* C) . (m + 1) is_of_type {} ,I & the connectives of (B +* C) . m <> the connectives of (B +* C) . (m + 1) & the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I & the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
thus I <> the bool-sort of (B +* C) by A3, Def52; :: thesis: ( the connectives of (B +* C) . m is_of_type {} ,I & the connectives of (B +* C) . (m + 1) is_of_type {} ,I & the connectives of (B +* C) . m <> the connectives of (B +* C) . (m + 1) & the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I & the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )

A6: 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 ) )

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 A7: 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 A8: the connectives of B . i nin the carrier' of C by A4, XBOOLE_0:3;
A9: ( 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 A10: ( 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 A8, A9, FUNCT_4:11;
thus A11: the connectives of (B +* C) . i = the connectives of B . i by A5, A7, 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 A12: ( 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 A10, A12, A11; :: thesis: verum

end;

m + 0 <= m + 6 by XREAL_1:6;
then A13: ( 0 + 1 <= m & m <= len the connectives of B ) by A1, A2, XXREAL_0:2, NAT_1:13;
hence the connectives of (B +* C) . m is_of_type {} ,I by A6, A3; :: thesis: ( the connectives of (B +* C) . (m + 1) is_of_type {} ,I & the connectives of (B +* C) . m <> the connectives of (B +* C) . (m + 1) & the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I & the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
m + 1 <= m + 6 by XREAL_1:6;
then A14: ( 0 + 1 <= m + 1 & m + 1 <= len the connectives of B ) by A2, XXREAL_0:2, NAT_1:11;
hence the connectives of (B +* C) . (m + 1) is_of_type {} ,I by A6, A3; :: thesis: ( the connectives of (B +* C) . m <> the connectives of (B +* C) . (m + 1) & the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I & the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
( the connectives of (B +* C) . m = the connectives of B . m & the connectives of (B +* C) . (m + 1) = the connectives of B . (m + 1) ) by A13, A14, A6;
hence the connectives of (B +* C) . m <> the connectives of (B +* C) . (m + 1) by A3; :: thesis: ( the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I & the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
m + 2 <= m + 6 by XREAL_1:6;
then ( 0 + 1 <= m + 2 & m + 2 <= len the connectives of B ) by A2, XXREAL_0:2, NAT_1:12;
hence the connectives of (B +* C) . (m + 2) is_of_type <*I*>,I by A6, A3; :: thesis: ( the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
m + 3 <= m + 6 by XREAL_1:6;
then A15: ( 0 + 1 <= m + 3 & m + 3 <= len the connectives of B ) by A2, XXREAL_0:2, NAT_1:12;
hence the connectives of (B +* C) . (m + 3) is_of_type <*I,I*>,I by A3, A6; :: thesis: ( the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
m + 4 <= m + 6 by XREAL_1:6;
then A16: ( 0 + 1 <= m + 4 & m + 4 <= len the connectives of B ) by A2, XXREAL_0:2, NAT_1:12;
hence the connectives of (B +* C) . (m + 4) is_of_type <*I,I*>,I by A3, A6; :: thesis: ( the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
m + 5 <= m + 6 by XREAL_1:6;
then A17: ( 0 + 1 <= m + 5 & m + 5 <= len the connectives of B ) by A2, XXREAL_0:2, NAT_1:12;
hence the connectives of (B +* C) . (m + 5) is_of_type <*I,I*>,I by A3, A6; :: thesis: ( the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) )
( the connectives of (B +* C) . (m + 3) = the connectives of B . (m + 3) & the connectives of (B +* C) . (m + 5) = the connectives of B . (m + 5) & the connectives of (B +* C) . (m + 4) = the connectives of B . (m + 4) ) by A15, A16, A17, A6;
hence ( the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 4) & the connectives of (B +* C) . (m + 3) <> the connectives of (B +* C) . (m + 5) & the connectives of (B +* C) . (m + 4) <> the connectives of (B +* C) . (m + 5) ) by A3; :: thesis: the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C)
( 0 + 1 <= m + 6 & the bool-sort of (B +* C) = the bool-sort of B ) by Def52, NAT_1:12;
hence the connectives of (B +* C) . (m + 6) is_of_type <*I,I*>, the bool-sort of (B +* C) by A2, A3, A6; :: thesis: verum