let D1 be non empty set ; :: thesis: for f being FinSequence of PFuncs (D1,REAL)
for d being Element of D1
for n being Element of NAT holds (f | n) # d = (f # d) | n
let f be FinSequence of PFuncs (D1,REAL); :: thesis: for d being Element of D1
for n being Element of NAT holds (f | n) # d = (f # d) | n
let d1 be Element of D1; :: thesis: for n being Element of NAT holds (f | n) # d1 = (f # d1) | n
let n be Element of NAT ; :: thesis: (f | n) # d1 = (f # d1) | n
A1: len (f # d1) = len f by Def8;
A2: len ((f | n) # d1) = len (f | n) by Def8;

now

per cases ( len f <= n or n < len f ) ;

case A3: len f <= n ; :: thesis: (f | n) # d1 = (f # d1) | n

then f | n = f by Lm1;
hence (f | n) # d1 = (f # d1) | n by A1, A3, Lm1; :: thesis: verum

end;

case A4: n < len f ; :: thesis: (f | n) # d1 = (f # d1) | n

then A5: len (f | n) = n by FINSEQ_1:59;
A6: len ((f # d1) | n) = n by A1, A4, FINSEQ_1:59;
A7: ( dom f = Seg (len f) & dom (f # d1) = Seg (len (f # d1)) ) by FINSEQ_1:def 3;
A8: dom ((f | n) # d1) = Seg (len ((f | n) # d1)) by FINSEQ_1:def 3;

now

per cases ( n = 0 or n <> 0 ) ;

case A9: n = 0 ; :: thesis: (f | n) # d1 = (f # d1) | n

then (f # d1) | n = <*> REAL ;
hence (f | n) # d1 = (f # d1) | n by A2, A9; :: thesis: verum

end;

case A10: n <> 0 ; :: thesis: (f | n) # d1 = (f # d1) | n

A11: dom ((f # d1) | n) = Seg (len (f | n)) by A5, A6, FINSEQ_1:def 3;
0 + 1 <= n by A10, NAT_1:13;
then A12: n in dom f by A4, FINSEQ_3:25;

now

let m be Nat; :: thesis: ( m in dom ((f # d1) | n) implies ((f # d1) | n) . m = ((f | n) # d1) . m )
assume A13: m in dom ((f # d1) | n) ; :: thesis: ((f # d1) | n) . m = ((f | n) # d1) . m
then A14: m in dom (f # d1) by A1, A5, A7, A12, A11, RFINSEQ:6;
then reconsider G = f . m as Element of PFuncs (D1,REAL) by A1, A7, FINSEQ_2:11;
((f # d1) | n) . m = (f # d1) . m by A1, A5, A7, A12, A11, A13, RFINSEQ:6;
then A15: ((f # d1) | n) . m = G . d1 by A14, Def8;
(f | n) . m = G by A5, A12, A11, A13, RFINSEQ:6;
hence ((f # d1) | n) . m = ((f | n) # d1) . m by A2, A8, A11, A13, A15, Def8; :: thesis: verum

end;

hence (f | n) # d1 = (f # d1) | n by A2, A5, A6, FINSEQ_2:9; :: thesis: verum

end;

end;

end;

hence (f | n) # d1 = (f # d1) | n ; :: thesis: verum

end;

end;

end;

hence (f | n) # d1 = (f # d1) | n ; :: thesis: verum