let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l being Nat ex k being Nat st l = il. (T,k)
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for l being Nat ex k being Nat st l = il. (T,k)
let l be Nat; :: thesis: ex k being Nat st l = il. (T,k)
consider f1 being sequence of 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 Def4;
( l in NAT & rng f1 = NAT ) by A1, FUNCT_2:def 3, ORDINAL1:def 12;
then consider k being object 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, Def4;
hence l = il. (T,k) ; :: thesis: verum