let D, D9, E be non empty set ; :: thesis: for d being Element of D

for d9 being Element of D9

for i 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 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 natural Number

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 natural Number

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 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 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 CARD_1:def 7;

then A2: len (T9 ^ <*d9*>) = i + 1 by FINSEQ_2:16;

A3: len T = i by CARD_1:def 7;

then A4: len (F .: (T,T9)) = i by A1, FINSEQ_2:72;

len (T ^ <*d*>) = i + 1 by A3, FINSEQ_2:16;

then A5: len (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = i + 1 by A2, FINSEQ_2:72;

then A6: dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = Seg (i + 1) by FINSEQ_1:def 3;

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

for d9 being Element of D9

for i 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 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 natural Number

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 natural Number

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 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 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 CARD_1:def 7;

then A2: len (T9 ^ <*d9*>) = i + 1 by FINSEQ_2:16;

A3: len T = i by CARD_1:def 7;

then A4: len (F .: (T,T9)) = i by A1, FINSEQ_2:72;

len (T ^ <*d*>) = i + 1 by A3, FINSEQ_2:16;

then A5: len (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = i + 1 by A2, FINSEQ_2:72;

then A6: dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) = Seg (i + 1) by FINSEQ_1:def 3;

A7: now :: thesis: for j being Nat st j in dom (F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) holds

(F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j

len ((F .: (T,T9)) ^ <*(F . (d,d9))*>) = (len (F .: (T,T9))) + 1
by FINSEQ_2:16;(F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j

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

end;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 :: thesis: F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . jend;

hence
(F .: ((T ^ <*d*>),(T9 ^ <*d9*>))) . j = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j
by A8, FUNCOP_1:22; :: thesis: verumper cases
( j in Seg i or j = i + 1 )
by A6, A8, FINSEQ_2:7;

end;

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:22

.= ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A4, A9, A11, FINSEQ_1:def 7 ;

:: thesis: verum

end;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:22

.= ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A4, A9, A11, FINSEQ_1:def 7 ;

:: thesis: verum

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:42;

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

end;hence F . (((T ^ <*d*>) . j),((T9 ^ <*d9*>) . j)) = ((F .: (T,T9)) ^ <*(F . (d,d9))*>) . j by A4, A13, FINSEQ_1:42; :: thesis: verum

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