let D, D9, E 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:78;
len (p9 ^ <*d9*>) = (len p9) + 1 by FINSEQ_2:16;
then A2: len (F [;] (d,(p9 ^ <*d9*>))) = (len p9) + 1 by FINSEQ_2:78;
then A3: dom (F [;] (d,(p9 ^ <*d9*>))) = Seg ((len p9) + 1) by FINSEQ_1:def 3;
A4: now :: thesis: for j being Nat st j in dom (F [;] (d,(p9 ^ <*d9*>))) holds
(F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j
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 :: thesis: F . (d,((p9 ^ <*d9*>) . j)) = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j
per cases ( j in Seg (len p9) or j = (len p9) + 1 ) by ;
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 ;
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
.= (F [;] (d,p9)) . j by
.= ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by ;
:: 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:42
.= ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by ;
:: thesis: verum
end;
end;
end;
hence (F [;] (d,(p9 ^ <*d9*>))) . j = ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) . j by ; :: thesis: verum
end;
len ((F [;] (d,p9)) ^ <*(F . (d,d9))*>) = (len (F [;] (d,p9))) + 1 by FINSEQ_2:16;
hence F [;] (d,(p9 ^ <*d9*>)) = (F [;] (d,p9)) ^ <*(F . (d,d9))*> by ; :: thesis: verum