(len f) + (len g) >= (len f) + 0 by XREAL_1:6;
then A0: len (f ^ g) >= len f by Def1;
then A1: len ((f ^ g) | (len f)) = len f by AFINSQ_1:54;
for i being Nat st i in dom f holds
((f ^ g) | (len f)) . i = f . i

proof

let i be Nat; :: thesis: ( i in dom f implies ((f ^ g) | (len f)) . i = f . i )
assume B1: i in dom f ; :: thesis: ((f ^ g) | (len f)) . i = f . i
then f . i = (f ^ g) . i by Def1;
hence ((f ^ g) | (len f)) . i = f . i by A0, B1, AFINSQ_1:53; :: thesis: verum

end;

hence (f ^ g) | (len f) = f by A1; :: thesis: verum