let D, E, D9 be non empty set ; :: thesis: for d being Element of D
for d9 being Element of D9
for F being Function of [:D,D9:],E
for p9 being FinSequence of D9 holds F [;] d,(p9 ^ <*d9*>) = (F [;] d,p9) ^ <*(F . d,d9)*>
let d be Element of D; :: thesis: for d9 being Element of D9
for F being Function of [:D,D9:],E
for p9 being FinSequence of D9 holds F [;] d,(p9 ^ <*d9*>) = (F [;] d,p9) ^ <*(F . d,d9)*>
let d9 be Element of D9; :: thesis: for F being Function of [:D,D9:],E
for p9 being FinSequence of D9 holds F [;] d,(p9 ^ <*d9*>) = (F [;] d,p9) ^ <*(F . d,d9)*>
let F be Function of [:D,D9:],E; :: thesis: for p9 being FinSequence of D9 holds F [;] d,(p9 ^ <*d9*>) = (F [;] d,p9) ^ <*(F . d,d9)*>
let p9 be FinSequence of D9; :: thesis: F [;] d,(p9 ^ <*d9*>) = (F [;] d,p9) ^ <*(F . d,d9)*>
set pd = p9 ^ <*d9*>;
set q = F [;] d,p9;
set r = F [;] d,(p9 ^ <*d9*>);
set s = (F [;] d,p9) ^ <*(F . d,d9)*>;
set i = len p9;
A1: len (F [;] d,p9) = len p9 by FINSEQ_2:92;
len (p9 ^ <*d9*>) = (len p9) + 1 by FINSEQ_2:19;
then A2: len (F [;] d,(p9 ^ <*d9*>)) = (len p9) + 1 by FINSEQ_2:92;
then A3: dom (F [;] d,(p9 ^ <*d9*>)) = Seg ((len p9) + 1) by FINSEQ_1:def 3;

A4: now

let j be Nat; :: thesis: ( j in dom (F [;] d,(p9 ^ <*d9*>)) implies (F [;] d,(p9 ^ <*d9*>)) . j = ((F [;] d,p9) ^ <*(F . d,d9)*>) . j )
assume A5: j in dom (F [;] d,(p9 ^ <*d9*>)) ; :: thesis: (F [;] d,(p9 ^ <*d9*>)) . j = ((F [;] d,p9) ^ <*(F . d,d9)*>) . j

now

per cases ( j in Seg (len p9) or j = (len p9) + 1 ) by A3, A5, FINSEQ_2:8;

suppose A6: j in Seg (len p9) ; :: thesis: F . d,((p9 ^ <*d9*>) . j) = ((F [;] d,p9) ^ <*(F . d,d9)*>) . j

then A7: j in dom (F [;] d,p9) by A1, FINSEQ_1:def 3;
A8: Seg (len (F [;] d,p9)) = dom (F [;] d,p9) by FINSEQ_1:def 3;
Seg (len p9) = dom p9 by FINSEQ_1:def 3;
hence F . d,((p9 ^ <*d9*>) . j) = F . d,(p9 . j) by A6, FINSEQ_1:def 7
.= (F [;] d,p9) . j by A7, FUNCOP_1:42
.= ((F [;] d,p9) ^ <*(F . d,d9)*>) . j by A1, A6, A8, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A9: j = (len p9) + 1 ; :: thesis: F . d,((p9 ^ <*d9*>) . j) = ((F [;] d,p9) ^ <*(F . d,d9)*>) . j

hence F . d,((p9 ^ <*d9*>) . j) = F . d,d9 by FINSEQ_1:59
.= ((F [;] d,p9) ^ <*(F . d,d9)*>) . j by A1, A9, FINSEQ_1:59 ;
:: thesis: verum

end;

end;

end;

hence (F [;] d,(p9 ^ <*d9*>)) . j = ((F [;] d,p9) ^ <*(F . d,d9)*>) . j by A5, FUNCOP_1:42; :: thesis: verum

end;

len ((F [;] d,p9) ^ <*(F . d,d9)*>) = (len (F [;] d,p9)) + 1 by FINSEQ_2:19;
hence F [;] d,(p9 ^ <*d9*>) = (F [;] d,p9) ^ <*(F . d,d9)*> by A1, A2, A4, FINSEQ_2:10; :: thesis: verum