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 l1, l2 being Element of NAT st locnum l1,T = locnum l2,T holds
l1 = l2
let T be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of 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 Def13;
hence l1 = l2 by A1, Def13; :: thesis: verum