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 p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(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 p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let d9 be Element of D9; :: thesis: for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let F be Function of [:D,D9:],E; :: thesis: for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let p be FinSequence of D; :: thesis: F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
set pd = p ^ <*d*>;
set q = F [:] (p,d9);
set r = F [:] ((p ^ <*d*>),d9);
set s = (F [:] (p,d9)) ^ <*(F . (d,d9))*>;
set i = len p;
A1: len (F [:] (p,d9)) = len p by FINSEQ_2:84;
len (p ^ <*d*>) = (len p) + 1 by FINSEQ_2:16;
then A2: len (F [:] ((p ^ <*d*>),d9)) = (len p) + 1 by FINSEQ_2:84;
then A3: dom (F [:] ((p ^ <*d*>),d9)) = Seg ((len p) + 1) by FINSEQ_1:def 3;

A4: now :: thesis: for j being Nat st j in dom (F [:] ((p ^ <*d*>),d9)) holds
(F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j

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

now :: thesis: F . (((p ^ <*d*>) . j),d9) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j

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

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

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

end;

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

hence F . (((p ^ <*d*>) . j),d9) = F . (d,d9) by FINSEQ_1:42
.= ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j by A1, A8, FINSEQ_1:42 ;
:: thesis: verum

end;

end;

end;

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

end;

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