let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N holds
( S is standard iff ex f being Function of NAT ,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ) ) )
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: ( S is standard iff ex f being Function of NAT ,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ) ) )

hereby :: thesis: ( ex f being Function of NAT ,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ) ) implies S is standard )

assume S is standard ; :: thesis: ex f being Function of NAT ,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ) )
then consider f being Function of NAT ,NAT such that
A1: f is bijective and
A2: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) by Def10;
thus ex f being Function of NAT ,NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ) ) :: thesis: verum

proof

take f ; :: thesis: ( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ) )
thus f is bijective by A1; :: thesis: for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) )
thus for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) by A1, A2, Th18; :: thesis: verum

end;

end;

given f being Function of NAT ,NAT such that A3: f is bijective and
A4: for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k),S & ( for j being Element of NAT st f . j in SUCC (f . k),S holds
k <= j ) ) ; :: thesis: S is standard
take f ; :: according to AMISTD_1:def 10 :: thesis: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) )
thus f is bijective by A3; :: thesis: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S )
thus for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) by A3, A4, Th18; :: thesis: verum