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

A2: now

let k be Element of 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 Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A2); :: thesis: verum