let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for k1, k2 being natural number st il. T,k1 = il. T,k2 holds
k1 = k2
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for k1, k2 being natural number st il. T,k1 = il. T,k2 holds
k1 = k2
let k1, k2 be natural number ; :: thesis: ( il. T,k1 = il. T,k2 implies k1 = k2 )
assume A1: il. T,k1 = il. T,k2 ; :: thesis: k1 = k2
A2: ( k1 is Element of NAT & k2 is Element of NAT ) by ORDINAL1:def 13;
consider f1 being IL-Function of NAT ,T such that
A3: ( f1 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n ) ) & il. T,k1 = f1 . k1 ) by Def12;
consider f2 being IL-Function of NAT ,T such that
A4: ( f2 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n ) ) & il. T,k2 = f2 . k2 ) by Def12;
A5: f1 = f2 by A3, A4, Th17;
( f1 is one-to-one & dom f1 = NAT ) by A3, FUNCT_2:def 1;
hence k1 = k2 by A1, A2, A3, A4, A5, FUNCT_1:def 8; :: thesis: verum