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