let D, D9, E be non empty set ; :: thesis: for i, j being natural Number
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 natural Number ; :: 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))
A0: ( i is Nat & j is Nat ) by TARSKI:1;
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 :: thesis: for j being natural Number st ( 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)) ) holds
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 j be natural Number ; :: 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:117;
A3: T ^ S = (T ^ S1) ^ <*d*> by A2, FINSEQ_1:32;
reconsider S1 = S1 as Tuple of j,D ;
consider S19 being Element of j -tuples_on D9, d9 being Element of D9 such that
A4: S9 = S19 ^ <*d9*> by FINSEQ_2:117;
A5: T9 ^ S9 = (T9 ^ S19) ^ <*d9*> by A4, FINSEQ_1:32;
reconsider S19 = S19 as Tuple of j,D9 ;
thus F .: ((T ^ S),(T9 ^ S9)) = (F .: ((T ^ S1),(T9 ^ S19))) ^ <*(F . (d,d9))*> by A3, A5, Th10
.= ((F .: (T,T9)) ^ (F .: (S1,S19))) ^ <*(F . (d,d9))*> by A1
.= (F .: (T,T9)) ^ ((F .: (S1,S19)) ^ <*(F . (d,d9))*>) by FINSEQ_1:32
.= (F .: (T,T9)) ^ (F .: (S,S9)) by A2, A4, Th10 ; :: thesis: verum

end;

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

now :: thesis: for S being Tuple of 0 ,D
for S9 being Tuple of 0 ,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))

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:73;
( T ^ S = T & T9 ^ S9 = T9 ) by FINSEQ_2:95;
hence F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) by A7, FINSEQ_1:34; :: 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)) by A0; :: thesis: verum