let E, D, D9 be non empty set ; :: thesis: for i, j being Nat
for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let i, j be Nat; :: thesis: for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let F be Function of [:D,D9:],E; :: thesis: for T being Tuple of i,D
for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let T be Tuple of i,D; :: thesis: for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let T9 be Tuple of i,D9; :: thesis: for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let S be Tuple of j,D; :: thesis: for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let S9 be Tuple of j,D9; :: thesis: F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
defpred S₁[ Nat] means for S being Tuple of $1,D
for S9 being Tuple of $1,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9);

now

let j be Nat; :: thesis: ( ( for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9) ) implies for S being Tuple of j + 1,D
for S9 being Tuple of j + 1,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9) )
assume A1: for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9) ; :: thesis: for S being Tuple of j + 1,D
for S9 being Tuple of j + 1,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let S be Tuple of j + 1,D; :: thesis: for S9 being Tuple of j + 1,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let S9 be Tuple of j + 1,D9; :: thesis: F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
consider S1 being Element of j -tuples_on D, d being Element of D such that
A2: S = S1 ^ <*d*> by FINSEQ_2:137;
A3: T ^ S = (T ^ S1) ^ <*d*> by A2, FINSEQ_1:45;
reconsider S1 = S1 as Tuple of j,D by FINSEQ_2:151;
consider S19 being Element of j -tuples_on D9, d9 being Element of D9 such that
A4: S9 = S19 ^ <*d9*> by FINSEQ_2:137;
A5: T9 ^ S9 = (T9 ^ S19) ^ <*d9*> by A4, FINSEQ_1:45;
reconsider S19 = S19 as Tuple of j,D9 by FINSEQ_2:151;
( T ^ S1 is Tuple of i + j,D & T9 ^ S19 is Tuple of i + j,D9 ) by FINSEQ_2:127;
hence F .: (T ^ S),(T9 ^ S9) = (F .: (T ^ S1),(T9 ^ S19)) ^ <*(F . d,d9)*> by A3, A5, Th11
.= ((F .: T,T9) ^ (F .: S1,S19)) ^ <*(F . d,d9)*> by A1
.= (F .: T,T9) ^ ((F .: S1,S19) ^ <*(F . d,d9)*>) by FINSEQ_1:45
.= (F .: T,T9) ^ (F .: S,S9) by A2, A4, Th11 ;
:: thesis: verum

end;

then A6: for j being Nat st S₁[j] holds
S₁[j + 1] ;

now

let S be Tuple of 0 ,D; :: thesis: for S9 being Tuple of 0 ,D9 holds F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
let S9 be Tuple of 0 ,D9; :: thesis: F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
S = <*> D ;
then A7: F .: S,S9 = <*> E by FINSEQ_2:87;
( T ^ S = T & T9 ^ S9 = T9 ) by FINSEQ_2:115;
hence F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9) by A7, FINSEQ_1:47; :: thesis: verum

end;

then A8: S₁[ 0 ] ;
for j being Nat holds S₁[j] from NAT_1:sch 2(A8, A6);
hence F .: (T ^ S),(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9) ; :: thesis: verum