let RNS be non empty 1-sorted ; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: for n, k being Nat holds S . n = S . (n + k)
let n be Nat; :: thesis: for k being Nat holds S . n = S . (n + k)
defpred S₁[ Nat] means S . n = S . (n + $1);

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
S . (n + k) = S . ((n + k) + 1) by A1;
hence S₁[k + 1] by A3; :: thesis: verum

end;

A4: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2); :: thesis: verum