theorem Th62: :: AOFA_A00:67

for n, m being Nat
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