let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite 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 stored-program IC-Ins-separated definite 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 13;
then consider k being set such that
A3: k in dom f1 and
A4: f1 . k = l by FUNCT_1:def 5;
reconsider k = k as Nat by A3;
take k ; :: thesis: l = il. T,k
l in NAT by ORDINAL1:def 13;
then reconsider l = l as Element of NAT ;
l = il. T,k by A1, A2, A4, Def12;
hence l = il. T,k ; :: thesis: verum