deffunc H₁( Element of NAT ) -> Instruction-Location of SCM+FSA = insloc c₁;
A1: for k being Element of NAT holds H₁(k) 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 IL-Function of NAT , SCM+FSA by AMI_1:def 36;
A3: for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) by A2, Th85;
f is bijective by A2, Th85;
hence SCM+FSA is standard by A3, AMISTD_1:19; :: thesis: verum