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 & len ((f | n) # d1) = len (f | n) ) by Def8;

now

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

case A2: 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, A2, Lm1; :: thesis: verum

end;

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

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

now

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

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

then ( (f # d1) | n = <*> REAL & (f | n) # d1 = <*> REAL ) by A1;
hence (f | n) # d1 = (f # d1) | n ; :: thesis: verum

end;

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

then 0 < n ;
then 0 + 1 <= n by NAT_1:13;
then A6: n in dom f by A3, FINSEQ_3:27;
X: dom ((f # d1) | n) = Seg (len (f | n)) by A4, FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom ((f # d1) | n) implies ((f # d1) | n) . m = ((f | n) # d1) . m )
assume A7: m in dom ((f # d1) | n) ; :: thesis: ((f # d1) | n) . m = ((f | n) # d1) . m
then A8: ( ((f # d1) | n) . m = (f # d1) . m & m in dom (f # d1) ) by A1, A4, A5, A6, X, RFINSEQ:19;
then reconsider G = f . m as Element of PFuncs D1,REAL by A1, A5, FINSEQ_2:13;
A9: ((f # d1) | n) . m = G . d1 by A8, Def8;
( (f | n) . m = G & m in dom f ) by A4, A6, A7, X, RFINSEQ:19;
hence ((f # d1) | n) . m = ((f | n) # d1) . m by A1, A5, A7, A9, Def8, X; :: thesis: verum

end;

hence (f | n) # d1 = (f # d1) | n by A1, A4, FINSEQ_2:10; :: 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