let E, D, D9 be non empty set ; :: thesis: for d being Element of D
for d9 being Element of D9
for i being Nat
for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9 holds F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*>
let d be Element of D; :: thesis: for d9 being Element of D9
for i being Nat
for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9 holds F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*>
let d9 be Element of D9; :: thesis: for i being Nat
for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9 holds F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*>
let i 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 holds F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*>
let F be Function of [:D,D9:],E; :: thesis: for T being Tuple of i,D
for T9 being Tuple of i,D9 holds F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*>
let T be Tuple of i,D; :: thesis: for T9 being Tuple of i,D9 holds F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*>
let T9 be Tuple of i,D9; :: thesis: F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*>
set p = T ^ <*d*>;
set q = T9 ^ <*d9*>;
set pq = F .: T,T9;
set r = F .: (T ^ <*d*>),(T9 ^ <*d9*>);
set s = (F .: T,T9) ^ <*(F . d,d9)*>;
A1: len T9 = i by FINSEQ_1:def 18;
then A2: len (T9 ^ <*d9*>) = i + 1 by FINSEQ_2:19;
A3: len T = i by FINSEQ_1:def 18;
then A4: len (F .: T,T9) = i by A1, FINSEQ_2:86;
len (T ^ <*d*>) = i + 1 by A3, FINSEQ_2:19;
then A5: len (F .: (T ^ <*d*>),(T9 ^ <*d9*>)) = i + 1 by A2, FINSEQ_2:86;
then A6: dom (F .: (T ^ <*d*>),(T9 ^ <*d9*>)) = Seg (i + 1) by FINSEQ_1:def 3;

A7: now

let j be Nat; :: thesis: ( j in dom (F .: (T ^ <*d*>),(T9 ^ <*d9*>)) implies (F .: (T ^ <*d*>),(T9 ^ <*d9*>)) . j = ((F .: T,T9) ^ <*(F . d,d9)*>) . j )
assume A8: j in dom (F .: (T ^ <*d*>),(T9 ^ <*d9*>)) ; :: thesis: (F .: (T ^ <*d*>),(T9 ^ <*d9*>)) . j = ((F .: T,T9) ^ <*(F . d,d9)*>) . j

now

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

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

Seg (len T) = dom T by FINSEQ_1:def 3;
then A10: (T ^ <*d*>) . j = T . j by A3, A9, FINSEQ_1:def 7;
A11: Seg (len (F .: T,T9)) = dom (F .: T,T9) by FINSEQ_1:def 3;
Seg (len T9) = dom T9 by FINSEQ_1:def 3;
then A12: (T9 ^ <*d9*>) . j = T9 . j by A1, A9, FINSEQ_1:def 7;
j in dom (F .: T,T9) by A4, A9, FINSEQ_1:def 3;
hence F . ((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j) = (F .: T,T9) . j by A10, A12, FUNCOP_1:28
.= ((F .: T,T9) ^ <*(F . d,d9)*>) . j by A4, A9, A11, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

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

end;

end;

end;

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

end;

len ((F .: T,T9) ^ <*(F . d,d9)*>) = (len (F .: T,T9)) + 1 by FINSEQ_2:19;
hence F .: (T ^ <*d*>),(T9 ^ <*d9*>) = (F .: T,T9) ^ <*(F . d,d9)*> by A5, A4, A7, FINSEQ_2:10; :: thesis: verum