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

A4: now

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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