let N be with_zero set ; 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; for k1, k2 being Nat st il. (T,k1) = il. (T,k2) holds
k1 = k2
let k1, k2 be Nat; ( il. (T,k1) = il. (T,k2) implies k1 = k2 )
assume A1:
il. (T,k1) = il. (T,k2)
; 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; verum