let n, m be Nat; ( 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
; 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 ; 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 ; 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 ; ( C is m,I,N -array implies B +* C is n + m,I,N -array )
assume A2:
len the connectives of C >= m + 3
; AOFA_A00:def 50 ( 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 )
; 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; AOFA_A00:def 50 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
; 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
; 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
; ( 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; ( 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; AOFA_A00:def 8 ( 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; ( 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; AOFA_A00:def 8 ( 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; ( 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; AOFA_A00:def 8 ( 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; 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; AOFA_A00:def 8 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; verum