let z be Nat; :: thesis: for N being with_zero set
for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f, g being Element of NAT st f + (z,T) = g + (z,T) holds
f = g
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 f, g being Element of NAT st f + (z,T) = g + (z,T) holds
f = g
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over 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 Th5;
hence f = g by Th7; :: thesis: verum