consider f being IL-Function of NAT ,S such that
A1: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) ) by Def10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
take f . k ; :: thesis: ex f being IL-Function of NAT ,S st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & f . k = f . k )
take f ; :: thesis: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & f . k = f . k )
thus ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & f . k = f . k ) by A1; :: thesis: verum