let E, D, D' be non empty set ; :: thesis: for d being Element of D
for d' being Element of D'
for i 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' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
let d be Element of D; :: thesis: for d' being Element of D'
for i 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' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
let d' be Element of D'; :: thesis: for i 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' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
let i 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' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
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' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
let T be Element of i -tuples_on D; :: thesis: for T' being Element of i -tuples_on D' holds F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
let T' be Element of i -tuples_on D'; :: thesis: F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*>
set p = T ^ <*d*>;
set q = T' ^ <*d'*>;
set pq = F .: T,T';
set r = F .: (T ^ <*d*>),(T' ^ <*d'*>);
set s = (F .: T,T') ^ <*(F . d,d')*>;
A1: ( len T = i & len T' = i ) by FINSEQ_2:109;
then ( len (T ^ <*d*>) = i + 1 & len (T' ^ <*d'*>) = i + 1 ) by FINSEQ_2:19;
then A2: len (F .: (T ^ <*d*>),(T' ^ <*d'*>)) = i + 1 by FINSEQ_2:86;
A3: len (F .: T,T') = i by A1, FINSEQ_2:86;
A4: len ((F .: T,T') ^ <*(F . d,d')*>) = (len (F .: T,T')) + 1 by FINSEQ_2:19;
X: dom (F .: (T ^ <*d*>),(T' ^ <*d'*>)) = Seg (i + 1) by A2, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom (F .: (T ^ <*d*>),(T' ^ <*d'*>)) implies (F .: (T ^ <*d*>),(T' ^ <*d'*>)) . j = ((F .: T,T') ^ <*(F . d,d')*>) . j )
assume A5: j in dom (F .: (T ^ <*d*>),(T' ^ <*d'*>)) ; :: thesis: (F .: (T ^ <*d*>),(T' ^ <*d'*>)) . j = ((F .: T,T') ^ <*(F . d,d')*>) . j
then A6: j in dom (F .: (T ^ <*d*>),(T' ^ <*d'*>)) ;

now

per cases ( j in Seg i or j = i + 1 ) by A5, FINSEQ_2:8, X;

suppose A7: j in Seg i ; :: thesis: F . ((T ^ <*d*>) . j),((T' ^ <*d'*>) . j) = ((F .: T,T') ^ <*(F . d,d')*>) . j

then A8: j in dom (F .: T,T') by A3, FINSEQ_1:def 3;
A9: Seg (len (F .: T,T')) = dom (F .: T,T') by FINSEQ_1:def 3;
( Seg (len T) = dom T & Seg (len T') = dom T' ) by FINSEQ_1:def 3;
then ( (T ^ <*d*>) . j = T . j & (T' ^ <*d'*>) . j = T' . j ) by A1, A7, FINSEQ_1:def 7;
hence F . ((T ^ <*d*>) . j),((T' ^ <*d'*>) . j) = (F .: T,T') . j by A8, FUNCOP_1:28
.= ((F .: T,T') ^ <*(F . d,d')*>) . j by A3, A7, A9, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A10: j = i + 1 ; :: thesis: F . ((T ^ <*d*>) . j),((T' ^ <*d'*>) . j) = ((F .: T,T') ^ <*(F . d,d')*>) . j

then ( (T ^ <*d*>) . j = d & (T' ^ <*d'*>) . j = d' ) by A1, FINSEQ_1:59;
hence F . ((T ^ <*d*>) . j),((T' ^ <*d'*>) . j) = ((F .: T,T') ^ <*(F . d,d')*>) . j by A3, A10, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

hence (F .: (T ^ <*d*>),(T' ^ <*d'*>)) . j = ((F .: T,T') ^ <*(F . d,d')*>) . j by A6, FUNCOP_1:28; :: thesis: verum

end;

hence F .: (T ^ <*d*>),(T' ^ <*d'*>) = (F .: T,T') ^ <*(F . d,d')*> by A2, A3, A4, FINSEQ_2:10; :: thesis: verum