deffunc H₁( Element of NAT ) -> Element of NAT = R;
A1: for x being Element of NAT holds H₁(x) is Element of NAT ;
consider f being Function of NAT ,NAT such that
A2: for k being Element of NAT holds f . k = H₁(k) from FUNCT_2:sch 9(A1);
reconsider f = f as Function of NAT ,NAT ;
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),(SCM R) & ( for j being Element of NAT st f . j in SUCC (f . k),(SCM R) holds
k <= j ) ) ) ) by A2, Th65;
hence SCM R is standard by AMISTD_1:19; :: thesis: verum