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