for x being Nat st x in dom f holds
f . x = ((f ^ seq) | (dom f)) . x

proof

let x be Nat; :: thesis: ( x in dom f implies f . x = ((f ^ seq) | (dom f)) . x )
assume A1: x in dom f ; :: thesis: f . x = ((f ^ seq) | (dom f)) . x
A1a: f \/ (f ^ seq) = f ^ seq by XBOOLE_1:6;
(dom f) /\ ((dom f) \/ (dom (Shift (seq,(len f))))) = dom f by XBOOLE_1:21;
then x in (dom f) /\ (dom (f ^ seq)) by A1, XTUPLE_0:23;
then f . x = (f ^ seq) . x by A1a, PARTFUN1:2
.= ((f ^ seq) | (dom f)) . x by A1, FUNCT_1:49 ;
hence f . x = ((f ^ seq) | (dom f)) . x ; :: thesis: verum

end;

hence (f ^ seq) | (dom f) = f ; :: thesis: verum