let RNS be non empty 1-sorted ; for S being sequence of RNS st ( for n being Nat holds S . n = S . (n + 1) ) holds
for n, k being Nat holds S . n = S . (n + k)
let S be sequence of RNS; ( ( for n being Nat holds S . n = S . (n + 1) ) implies for n, k being Nat holds S . n = S . (n + k) )
assume A1:
for n being Nat holds S . n = S . (n + 1)
; for n, k being Nat holds S . n = S . (n + k)
let n be Nat; for k being Nat holds S . n = S . (n + k)
defpred S1[ Nat] means S . n = S . (n + $1);
A2:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A3:
S1[
k]
;
S1[k + 1]
S . (n + k) = S . ((n + k) + 1)
by A1;
hence
S1[
k + 1]
by A3;
verum end;
A4:
S1[ 0 ]
;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A2); verum