let RNS be non empty 1-sorted ; :: thesis: for S being sequence of RNS st ( for n, k being Nat holds S . n = S . (n + k) ) holds
for n, m being Nat holds S . n = S . m
let S be sequence of RNS; :: thesis: ( ( for n, k being Nat holds S . n = S . (n + k) ) implies for n, m being Nat holds S . n = S . m )
assume A1: for n, k being Nat holds S . n = S . (n + k) ; :: thesis: for n, m being Nat holds S . n = S . m
let n, m be Nat; :: thesis: S . n = S . m
A2: now :: thesis: ( m <= n implies S . n = S . m )
assume m <= n ; :: thesis: S . n = S . m
then consider k being Nat such that
A3: n = m + k by NAT_1:10;
reconsider k = k as Nat ;
n = m + k by A3;
hence S . n = S . m by A1; :: thesis: verum
end;
now :: thesis: ( n <= m implies S . n = S . m )
assume n <= m ; :: thesis: S . n = S . m
then consider k being Nat such that
A4: m = n + k by NAT_1:10;
reconsider k = k as Nat ;
m = n + k by A4;
hence S . n = S . m by A1; :: thesis: verum
end;
hence S . n = S . m by A2; :: thesis: verum