let RNS be non empty 1-sorted ; :: thesis: for S being sequence of RNS st ( for n, k being Element of NAT holds S . n = S . (n + k) ) holds
for n, m being Element of NAT holds S . n = S . m
let S be sequence of RNS; :: thesis: ( ( for n, k being Element of NAT holds S . n = S . (n + k) ) implies for n, m being Element of NAT holds S . n = S . m )
assume A1: for n, k being Element of NAT holds S . n = S . (n + k) ; :: thesis: for n, m being Element of NAT holds S . n = S . m
let n, m be Element of NAT ; :: thesis: S . n = S . m

A2: now

assume n <= m ; :: thesis: S . n = S . m
then consider k being Nat such that
A3: m = n + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
m = n + k by A3;
hence S . n = S . m by A1; :: thesis: verum

end;

now

assume m <= n ; :: thesis: S . n = S . m
then consider k being Nat such that
A4: n = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n = m + k by A4;
hence S . n = S . m by A1; :: thesis: verum

end;

hence S . n = S . m by A2; :: thesis: verum