let x, y be object ; FUNCT_1:def 4 ( 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 that
A1:
x in dom (f /^ n)
and
A2:
y in dom (f /^ n)
and
A3:
(f /^ n) . x = (f /^ n) . y
; x = y
reconsider nx = x, ny = y as Nat by A1, A2;
A4:
nx < len (f /^ n)
by A1, AFINSQ_1:86;
A5:
len (f /^ n) = (len f) -' n
by Def2;
A6:
ny < len (f /^ n)
by A2, AFINSQ_1:86;
per cases
( n <= len f or n > len f )
;
suppose
n <= len f
;
x = ythen A7:
(len f) -' n = (len f) - n
by XREAL_1:233;
then A8:
nx + n < len f
by A4, A5, XREAL_1:20;
then A9:
nx + n in dom f
by AFINSQ_1:86;
A10:
ny + n < len f
by A6, A5, A7, XREAL_1:20;
then A11:
ny + n in dom f
by AFINSQ_1:86;
A12:
(f /^ n) . ny = f . (ny + n)
by A10, Th8;
(f /^ n) . nx = f . (nx + n)
by A8, Th8;
then
nx + n = ny + n
by A3, A9, A12, A11, FUNCT_1:def 4;
hence
x = y
;
verum end;