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 l1, l2 being Element of NAT st locnum (l1,T) = locnum (l2,T) holds
l1 = l2
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for l1, l2 being Element of NAT st locnum (l1,T) = locnum (l2,T) holds
l1 = l2
let l1, l2 be Element of NAT ; :: thesis: ( locnum (l1,T) = locnum (l2,T) implies l1 = l2 )
assume A1: locnum (l1,T) = locnum (l2,T) ; :: thesis: l1 = l2
il. (T,(locnum (l1,T))) = l1 by Def5;
hence l1 = l2 by A1, Def5; :: thesis: verum