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

now

let j be Nat; :: thesis: ( ( for S being Tuple of j,
for S' being Tuple of j, holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') ) implies for S being Tuple of j + 1,
for S' being Tuple of j + 1, holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') )
assume A1: for S being Tuple of j,
for S' being Tuple of j, holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') ; :: thesis: for S being Tuple of j + 1,
for S' being Tuple of j + 1, holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S be Tuple of j + 1, ; :: thesis: for S' being Tuple of j + 1, holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S' be Tuple of j + 1, ; :: thesis: F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
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, by FINSEQ_2:151;
consider S1' being Element of j -tuples_on D', d' being Element of D' such that
A4: S' = S1' ^ <*d'*> by FINSEQ_2:137;
A5: T' ^ S' = (T' ^ S1') ^ <*d'*> by A4, FINSEQ_1:45;
reconsider S1' = S1' as Tuple of j, by FINSEQ_2:151;
( T ^ S1 is Tuple of i + j, & T' ^ S1' is Tuple of i + j, ) by FINSEQ_2:127;
hence F .: (T ^ S),(T' ^ S') = (F .: (T ^ S1),(T' ^ S1')) ^ <*(F . d,d')*> by A3, A5, Th11
.= ((F .: T,T') ^ (F .: S1,S1')) ^ <*(F . d,d')*> by A1
.= (F .: T,T') ^ ((F .: S1,S1') ^ <*(F . d,d')*>) by FINSEQ_1:45
.= (F .: T,T') ^ (F .: S,S') 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 , ; :: thesis: for S' being Tuple of 0 , holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S' be Tuple of 0 , ; :: thesis: F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
S = <*> D ;
then A7: F .: S,S' = <*> E by FINSEQ_2:87;
( T ^ S = T & T' ^ S' = T' ) by FINSEQ_2:115;
hence F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') 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),(T' ^ S') = (F .: T,T') ^ (F .: S,S') ; :: thesis: verum