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 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 weakly_standard AMI-Struct of 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 f2 being Function of NAT,NAT such that
A3: ( f2 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f2 . m <= f2 . n,T ) ) ) and
A4: il. (T,k2) = f2 . k2 by Def12;
consider f1 being Function of NAT,NAT such that
A5: f1 is bijective and
A6: for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n,T ) and
A7: il. (T,k1) = f1 . k1 by Def12;
A8: dom f1 = NAT by FUNCT_2:def 1;
f1 = f2 by A5, A6, A3, Th17;
hence k1 = k2 by A1, A2, A5, A7, A4, A8, FUNCT_1:def 8; :: thesis: verum