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

now

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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