let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty IC-Ins-separated weakly_standard AMI-Struct of N
for l being Nat ex k being natural number st l = il. (T,k)
let T be non empty IC-Ins-separated weakly_standard AMI-Struct of N; :: thesis: for l being Nat ex k being natural number st l = il. (T,k)
let l be Nat; :: thesis: ex k being natural number st l = il. (T,k)
consider f1 being Function of NAT,NAT such that
A1: f1 is bijective and
A2: for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n,T ) and
il. (T,0) = f1 . 0 by Def12;
( l in NAT & rng f1 = NAT ) by A1, FUNCT_2:def 3, ORDINAL1:def 12;
then consider k being set such that
A3: k in dom f1 and
A4: f1 . k = l by FUNCT_1:def 3;
reconsider k = k as Nat by A3;
take k ; :: thesis: l = il. (T,k)
reconsider l = l as Element of NAT by ORDINAL1:def 12;
l = il. (T,k) by A1, A2, A4, Def12;
hence l = il. (T,k) ; :: thesis: verum