let z be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for T being non empty IC-Ins-separated weakly_standard AMI-Struct of N
for f, g being Element of NAT st f + (z,T) = g + (z,T) holds
f = g
let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty IC-Ins-separated weakly_standard AMI-Struct of N
for f, g being Element of NAT st f + (z,T) = g + (z,T) holds
f = g
let T be non empty IC-Ins-separated weakly_standard AMI-Struct of N; :: thesis: for f, g being Element of NAT st f + (z,T) = g + (z,T) holds
f = g
let f, g be Element of NAT ; :: thesis: ( f + (z,T) = g + (z,T) implies f = g )
assume f + (z,T) = g + (z,T) ; :: thesis: f = g
then (locnum (f,T)) + z = (locnum (g,T)) + z by Th25;
hence f = g by Th27; :: thesis: verum