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 Element of i -tuples_on D
for T' being Element of i -tuples_on D'
for S being Element of j -tuples_on D
for S' being Element of j -tuples_on D' 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 Element of i -tuples_on D
for T' being Element of i -tuples_on D'
for S being Element of j -tuples_on D
for S' being Element of j -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let F be Function of [:D,D':],E; :: thesis: for T being Element of i -tuples_on D
for T' being Element of i -tuples_on D'
for S being Element of j -tuples_on D
for S' being Element of j -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let T be Element of i -tuples_on D; :: thesis: for T' being Element of i -tuples_on D'
for S being Element of j -tuples_on D
for S' being Element of j -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let T' be Element of i -tuples_on D'; :: thesis: for S being Element of j -tuples_on D
for S' being Element of j -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S be Element of j -tuples_on D; :: thesis: for S' being Element of j -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S' be Element of j -tuples_on D'; :: thesis: F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
defpred S₁[ Nat] means for S being Element of $1 -tuples_on D
for S' being Element of $1 -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S');

now

let S be Element of 0 -tuples_on D; :: thesis: for S' being Element of 0 -tuples_on D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S' be Element of 0 -tuples_on D'; :: thesis: F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
S = <*> D by FINSEQ_2:113;
then ( T ^ S = T & T' ^ S' = T' & F .: S,S' = <*> E & <*> E = {} ) by FINSEQ_2:87, FINSEQ_2:115;
hence F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') by FINSEQ_1:47; :: thesis: verum

end;

then A1: S₁[ 0 ] ;

now

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

end;

then A5: for j being Nat st S₁[j] holds
S₁[j + 1] ;
for j being Nat holds S₁[j] from NAT_1:sch 2(A1, A5);
hence F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') ; :: thesis: verum