let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom (f /^ n) or not y in dom (f /^ n) or not (f /^ n) . x = (f /^ n) . y or x = y )
assume B1: ( x in dom (f /^ n) & y in dom (f /^ n) & (f /^ n) . x = (f /^ n) . y ) ; :: thesis: x = y
reconsider nx = x, ny = y as Nat by B1;
B3: ( nx < len (f /^ n) & ny < len (f /^ n) ) by B1, NAT_1:45;
B6: len (f /^ n) = (len f) -' n by Def2;

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

suppose n <= len f ; :: thesis: x = y

then C2: (len f) -' n = (len f) - n by XREAL_1:235;
nx + n < len f by C2, B3, B6, XREAL_1:22;
then C3: ( (f /^ n) . nx = f . (nx + n) & nx + n in dom f ) by Th19b, NAT_1:45;
ny + n < len f by C2, B3, B6, XREAL_1:22;
then ( (f /^ n) . ny = f . (ny + n) & ny + n in dom f ) by Th19b, NAT_1:45;
then nx + n = ny + n by C3, B1, FUNCT_1:def 8;
hence x = y ; :: thesis: verum

end;

suppose n > len f ; :: thesis: x = y

then f /^ n = {} by TH80e;
hence x = y by B1; :: thesis: verum

end;

end;