let n, m be Nat; :: thesis: ( m > 0 implies for B being non empty non void n -connectives BoolSignature
for I, N being set
for C being non empty non void ConnectivesSignature st C is m,I,N -array holds
B +* C is n + m,I,N -array )
assume A1: m > 0 ; :: thesis: for B being non empty non void n -connectives BoolSignature
for I, N being set
for C being non empty non void ConnectivesSignature st C is m,I,N -array holds
B +* C is n + m,I,N -array
let B be non empty non void n -connectives BoolSignature ; :: thesis: for I, N being set
for C being non empty non void ConnectivesSignature st C is m,I,N -array holds
B +* C is n + m,I,N -array
let I, N be set ; :: thesis: for C being non empty non void ConnectivesSignature st C is m,I,N -array holds
B +* C is n + m,I,N -array
let C be non empty non void ConnectivesSignature ; :: thesis: ( C is m,I,N -array implies B +* C is n + m,I,N -array )
assume A2: len the connectives of C >= m + 3 ; :: according to AOFA_A00:def 50 :: thesis: ( for J, K, L being Element of C holds
( not L = I or not K = N or not J <> L or not J <> K or not the connectives of C . m is_of_type <*J,K*>,L or not the connectives of C . (m + 1) is_of_type <*J,K,L*>,J or not the connectives of C . (m + 2) is_of_type <*J*>,K or not the connectives of C . (m + 3) is_of_type <*K,L*>,J ) or B +* C is n + m,I,N -array )
given J, K, L being Element of C such that A3: ( L = I & K = N & J <> L & J <> K & the connectives of C . m is_of_type <*J,K*>,L & the connectives of C . (m + 1) is_of_type <*J,K,L*>,J & the connectives of C . (m + 2) is_of_type <*J*>,K & the connectives of C . (m + 3) is_of_type <*K,L*>,J ) ; :: thesis: B +* C is n + m,I,N -array
set S = B +* C;
A4: len the connectives of B = n by Def29;
A5: the connectives of (B +* C) = the connectives of B ^ the connectives of C by Def52;
then A6: len the connectives of (B +* C) = n + (len the connectives of C) by A4, FINSEQ_1:22;
n + (m + 3) = (n + m) + 3 ;
hence len the connectives of (B +* C) >= (n + m) + 3 by A2, A6, XREAL_1:6; :: according to AOFA_A00:def 50 :: thesis: ex J, K, L being Element of (B +* C) st
( L = I & K = N & J <> L & J <> K & the connectives of (B +* C) . (n + m) is_of_type <*J,K*>,L & the connectives of (B +* C) . ((n + m) + 1) is_of_type <*J,K,L*>,J & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J*>,K & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K,L*>,J )
the carrier of (B +* C) = the carrier of B \/ the carrier of C by Th51;
then reconsider J0 = J, K0 = K, L0 = L as Element of (B +* C) by XBOOLE_0:def 3;
take J0 ; :: thesis: ex K, L being Element of (B +* C) st
( L = I & K = N & J0 <> L & J0 <> K & the connectives of (B +* C) . (n + m) is_of_type <*J0,K*>,L & the connectives of (B +* C) . ((n + m) + 1) is_of_type <*J0,K,L*>,J0 & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K,L*>,J0 )
take K0 ; :: thesis: ex L being Element of (B +* C) st
( L = I & K0 = N & J0 <> L & J0 <> K0 & the connectives of (B +* C) . (n + m) is_of_type <*J0,K0*>,L & the connectives of (B +* C) . ((n + m) + 1) is_of_type <*J0,K0,L*>,J0 & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L*>,J0 )
take L0 ; :: thesis: ( L0 = I & K0 = N & J0 <> L0 & J0 <> K0 & the connectives of (B +* C) . (n + m) is_of_type <*J0,K0*>,L0 & the connectives of (B +* C) . ((n + m) + 1) is_of_type <*J0,K0,L0*>,J0 & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0 )
thus ( L0 = I & K0 = N & J0 <> L0 & J0 <> K0 ) by A3; :: thesis: ( the connectives of (B +* C) . (n + m) is_of_type <*J0,K0*>,L0 & the connectives of (B +* C) . ((n + m) + 1) is_of_type <*J0,K0,L0*>,J0 & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0 )
m + 0 <= m + 3 by XREAL_1:6;
then ( 0 + 1 <= m & m <= len the connectives of C ) by A1, A2, XXREAL_0:2, NAT_1:13;
then A7: m in dom the connectives of C by FINSEQ_3:25;
A8: dom the Arity of C = the carrier' of C by FUNCT_2:def 1;
A9: the Arity of (B +* C) = the Arity of B +* the Arity of C by Th51;
then A10: the Arity of (B +* C) . ( the connectives of C . m) = the Arity of C . ( the connectives of C . m) by A7, A8, FUNCT_1:102, FUNCT_4:13;
A11: the connectives of (B +* C) . (n + m) = the connectives of C . m by A4, A5, A7, FINSEQ_1:def 7;
hence the Arity of (B +* C) . ( the connectives of (B +* C) . (n + m)) = <*J0,K0*> by A3, A10; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of (B +* C) . ( the connectives of (B +* C) . (n + m)) = L0 & the connectives of (B +* C) . ((n + m) + 1) is_of_type <*J0,K0,L0*>,J0 & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0 )
A12: dom the ResultSort of C = the carrier' of C by FUNCT_2:def 1;
A13: the ResultSort of (B +* C) = the ResultSort of B +* the ResultSort of C by Th51;
then the ResultSort of (B +* C) . ( the connectives of C . m) = the ResultSort of C . ( the connectives of C . m) by A7, A12, FUNCT_1:102, FUNCT_4:13;
hence the ResultSort of (B +* C) . ( the connectives of (B +* C) . (n + m)) = L0 by A3, A11; :: thesis: ( the connectives of (B +* C) . ((n + m) + 1) is_of_type <*J0,K0,L0*>,J0 & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0 )
m + 1 <= m + 3 by XREAL_1:6;
then ( 1 <= m + 1 & m + 1 <= len the connectives of C ) by A2, XXREAL_0:2, NAT_1:11;
then A14: m + 1 in dom the connectives of C by FINSEQ_3:25;
A15: the Arity of (B +* C) . ( the connectives of C . (m + 1)) = the Arity of C . ( the connectives of C . (m + 1)) by A14, A8, A9, FUNCT_1:102, FUNCT_4:13;
(n + m) + 1 = n + (m + 1) ;
then A16: the connectives of (B +* C) . ((n + m) + 1) = the connectives of C . (m + 1) by A4, A5, A14, FINSEQ_1:def 7;
hence the Arity of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 1)) = <*J0,K0,L0*> by A3, A15; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 1)) = J0 & the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0 )
the ResultSort of (B +* C) . ( the connectives of C . (m + 1)) = the ResultSort of C . ( the connectives of C . (m + 1)) by A14, A12, A13, FUNCT_1:102, FUNCT_4:13;
hence the ResultSort of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 1)) = J0 by A3, A16; :: thesis: ( the connectives of (B +* C) . ((n + m) + 2) is_of_type <*J0*>,K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0 )
m + 2 <= (m + 2) + 1 by NAT_1:11;
then m + 2 <= len the connectives of C by A2, XXREAL_0:2;
then A17: m + 2 in dom the connectives of C by NAT_1:12, FINSEQ_3:25;
A18: the Arity of (B +* C) . ( the connectives of C . (m + 2)) = the Arity of C . ( the connectives of C . (m + 2)) by A17, A8, A9, FUNCT_1:102, FUNCT_4:13;
(n + m) + 2 = n + (m + 2) ;
then A19: the connectives of (B +* C) . ((n + m) + 2) = the connectives of C . (m + 2) by A4, A5, A17, FINSEQ_1:def 7;
hence the Arity of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 2)) = <*J0*> by A3, A18; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 2)) = K0 & the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0 )
the ResultSort of (B +* C) . ( the connectives of C . (m + 2)) = the ResultSort of C . ( the connectives of C . (m + 2)) by A17, A12, A13, FUNCT_1:102, FUNCT_4:13;
hence the ResultSort of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 2)) = K0 by A3, A19; :: thesis: the connectives of (B +* C) . ((n + m) + 3) is_of_type <*K0,L0*>,J0
A20: m + 3 in dom the connectives of C by A2, NAT_1:12, FINSEQ_3:25;
A21: the Arity of (B +* C) . ( the connectives of C . (m + 3)) = the Arity of C . ( the connectives of C . (m + 3)) by A20, A8, A9, FUNCT_1:102, FUNCT_4:13;
(n + m) + 3 = n + (m + 3) ;
then A22: the connectives of (B +* C) . ((n + m) + 3) = the connectives of C . (m + 3) by A4, A5, A20, FINSEQ_1:def 7;
hence the Arity of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 3)) = <*K0,L0*> by A3, A21; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 3)) = J0
the ResultSort of (B +* C) . ( the connectives of C . (m + 3)) = the ResultSort of C . ( the connectives of C . (m + 3)) by A20, A12, A13, FUNCT_1:102, FUNCT_4:13;
hence the ResultSort of (B +* C) . ( the connectives of (B +* C) . ((n + m) + 3)) = J0 by A3, A22; :: thesis: verum