let n, m be Nat; :: thesis: for s, r being set
for S1, S2 being non empty ConnectivesSignature st 1 <= n & len the connectives of S1 >= n + 3 & ( for i being Nat st i >= n & i <= n + 3 holds
( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . (i + m)) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . (i + m)) ) ) & S2 is n + m,s,r -array holds
S1 is n,s,r -array
let s, r be set ; :: thesis: for S1, S2 being non empty ConnectivesSignature st 1 <= n & len the connectives of S1 >= n + 3 & ( for i being Nat st i >= n & i <= n + 3 holds
( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . (i + m)) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . (i + m)) ) ) & S2 is n + m,s,r -array holds
S1 is n,s,r -array
let S1, S2 be non empty ConnectivesSignature ; :: thesis: ( 1 <= n & len the connectives of S1 >= n + 3 & ( for i being Nat st i >= n & i <= n + 3 holds
( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . (i + m)) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . (i + m)) ) ) & S2 is n + m,s,r -array implies S1 is n,s,r -array )
assume A1: 1 <= n ; :: thesis: ( not len the connectives of S1 >= n + 3 or ex i being Nat st
( i >= n & i <= n + 3 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . (i + m)) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . (i + m)) ) ) or not S2 is n + m,s,r -array or S1 is n,s,r -array )
assume A2: len the connectives of S1 >= n + 3 ; :: thesis: ( ex i being Nat st
( i >= n & i <= n + 3 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . (i + m)) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . (i + m)) ) ) or not S2 is n + m,s,r -array or S1 is n,s,r -array )
assume A3: for i being Nat st i >= n & i <= n + 3 holds
( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . (i + m)) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . (i + m)) ) ; :: thesis: ( not S2 is n + m,s,r -array or S1 is n,s,r -array )
assume len the connectives of S2 >= (n + m) + 3 ; :: according to AOFA_A00:def 50 :: thesis: ( for J, K, L being Element of S2 holds
( not L = s or not K = r or not J <> L or not J <> K or not the connectives of S2 . (n + m) is_of_type <*J,K*>,L or not the connectives of S2 . ((n + m) + 1) is_of_type <*J,K,L*>,J or not the connectives of S2 . ((n + m) + 2) is_of_type <*J*>,K or not the connectives of S2 . ((n + m) + 3) is_of_type <*K,L*>,J ) or S1 is n,s,r -array )
given J, K, L being Element of S2 such that A4: ( L = s & K = r & J <> L & J <> K & the connectives of S2 . (n + m) is_of_type <*J,K*>,L & the connectives of S2 . ((n + m) + 1) is_of_type <*J,K,L*>,J & the connectives of S2 . ((n + m) + 2) is_of_type <*J*>,K & the connectives of S2 . ((n + m) + 3) is_of_type <*K,L*>,J ) ; :: thesis: S1 is n,s,r -array
thus len the connectives of S1 >= n + 3 by A2; :: according to AOFA_A00:def 50 :: thesis: ex J, K, L being Element of S1 st
( L = s & K = r & J <> L & J <> K & the connectives of S1 . n is_of_type <*J,K*>,L & the connectives of S1 . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S1 . (n + 2) is_of_type <*J*>,K & the connectives of S1 . (n + 3) is_of_type <*K,L*>,J )
A5: n <= n + 3 by NAT_1:11;
then ( the Arity of S1 . ( the connectives of S1 . n) = the Arity of S2 . ( the connectives of S2 . (n + m)) & the ResultSort of S1 . ( the connectives of S1 . n) = the ResultSort of S2 . ( the connectives of S2 . (n + m)) ) by A3;
then A6: ( the Arity of S1 . ( the connectives of S1 . n) = <*J,K*> & the ResultSort of S1 . ( the connectives of S1 . n) = L ) by A4;
A7: ( n <= n + 1 & n + 1 <= (n + 1) + 2 & n + 3 = (n + 1) + 2 ) by NAT_1:11;
then ( the Arity of S1 . ( the connectives of S1 . (n + 1)) = the Arity of S2 . ( the connectives of S2 . ((n + 1) + m)) & the ResultSort of S1 . ( the connectives of S1 . (n + 1)) = the ResultSort of S2 . ( the connectives of S2 . ((n + 1) + m)) ) by A3;
then A8: ( the Arity of S1 . ( the connectives of S1 . (n + 1)) = <*J,K,L*> & the ResultSort of S1 . ( the connectives of S1 . (n + 1)) = J ) by A4;
A9: ( n + 2 <= (n + 2) + 1 & n <= n + 2 ) by NAT_1:11;
then ( the Arity of S1 . ( the connectives of S1 . (n + 2)) = the Arity of S2 . ( the connectives of S2 . ((n + 2) + m)) & the ResultSort of S1 . ( the connectives of S1 . (n + 2)) = the ResultSort of S2 . ( the connectives of S2 . ((n + 2) + m)) ) by A3;
then A10: ( the Arity of S1 . ( the connectives of S1 . (n + 2)) = <*J*> & the ResultSort of S1 . ( the connectives of S1 . (n + 2)) = K ) by A4;
n <= n + 3 by NAT_1:11;
then ( the Arity of S1 . ( the connectives of S1 . (n + 3)) = the Arity of S2 . ( the connectives of S2 . ((n + 3) + m)) & the ResultSort of S1 . ( the connectives of S1 . (n + 3)) = the ResultSort of S2 . ( the connectives of S2 . ((n + 3) + m)) ) by A3;
then A11: ( the Arity of S1 . ( the connectives of S1 . (n + 3)) = <*K,L*> & the ResultSort of S1 . ( the connectives of S1 . (n + 3)) = J ) by A4;
( n <= len the connectives of S1 & 1 <= n + 1 & 1 <= (n + 1) + 1 & n + 1 <= len the connectives of S1 & n + 2 <= len the connectives of S1 & 1 <= n + 3 ) by A2, A5, A7, A9, XXREAL_0:2, NAT_1:11;
then ( n in dom the connectives of S1 & n + 1 in dom the connectives of S1 & n + 2 in dom the connectives of S1 ) by A1, FINSEQ_3:25;
then reconsider J = J, K = K, L = L as Element of S1 by A6, A8, A10, FUNCT_1:102, FUNCT_2:5;
take J ; :: thesis: ex K, L being Element of S1 st
( L = s & K = r & J <> L & J <> K & the connectives of S1 . n is_of_type <*J,K*>,L & the connectives of S1 . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S1 . (n + 2) is_of_type <*J*>,K & the connectives of S1 . (n + 3) is_of_type <*K,L*>,J )
take K ; :: thesis: ex L being Element of S1 st
( L = s & K = r & J <> L & J <> K & the connectives of S1 . n is_of_type <*J,K*>,L & the connectives of S1 . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S1 . (n + 2) is_of_type <*J*>,K & the connectives of S1 . (n + 3) is_of_type <*K,L*>,J )
take L ; :: thesis: ( L = s & K = r & J <> L & J <> K & the connectives of S1 . n is_of_type <*J,K*>,L & the connectives of S1 . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S1 . (n + 2) is_of_type <*J*>,K & the connectives of S1 . (n + 3) is_of_type <*K,L*>,J )
thus ( L = s & K = r & J <> L & J <> K ) by A4; :: thesis: ( the connectives of S1 . n is_of_type <*J,K*>,L & the connectives of S1 . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S1 . (n + 2) is_of_type <*J*>,K & the connectives of S1 . (n + 3) is_of_type <*K,L*>,J )
thus ( the connectives of S1 . n is_of_type <*J,K*>,L & the connectives of S1 . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S1 . (n + 2) is_of_type <*J*>,K & the connectives of S1 . (n + 3) is_of_type <*K,L*>,J ) by A6, A8, A10, A11; :: thesis: verum