let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 (f /^ n) or not y in proj1 (f /^ n) or not (f /^ n) . x = (f /^ n) . y or x = y )
assume that
A1: x in dom (f /^ n) and
A2: y in dom (f /^ n) and
A3: (f /^ n) . x = (f /^ n) . y ; :: thesis: x = y
reconsider nx = x, ny = y as Nat by A1, A2;
A4: nx < len (f /^ n) by A1, NAT_1:45;
A5: len (f /^ n) = (len f) -' n by Def2;
A6: ny < len (f /^ n) by A2, NAT_1:45;

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

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

then A7: (len f) -' n = (len f) - n by XREAL_1:235;
then A8: nx + n < len f by A4, A5, XREAL_1:22;
then A9: nx + n in dom f by NAT_1:45;
A10: ny + n < len f by A6, A5, A7, XREAL_1:22;
then A11: ny + n in dom f by NAT_1:45;
A12: (f /^ n) . ny = f . (ny + n) by A10, Th17;
(f /^ n) . nx = f . (nx + n) by A8, Th17;
then nx + n = ny + n by A3, A9, A12, A11, FUNCT_1:def 8;
hence x = y ; :: thesis: verum

end;

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

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

end;

end;