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

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

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

m + 0 <= m + 6
by XREAL_1:6;( 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;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

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