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 k1, k2 being Nat st il. (T,k1) = il. (T,k2) holds
k1 = k2
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for k1, k2 being Nat st il. (T,k1) = il. (T,k2) holds
k1 = k2
let k1, k2 be Nat; :: 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 12;
consider f2 being sequence of 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 Def4;
consider f1 being sequence of 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 Def4;
A8: dom f1 = NAT by FUNCT_2:def 1;
f1 = f2 by A5, A6, A3, Th2;
hence k1 = k2 by A1, A2, A5, A7, A4, A8, FUNCT_1:def 4; :: thesis: verum