let k be Nat; :: thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l being Element of NAT holds (l + (k,S)) -' (k,S) = l
let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for l being Element of NAT holds (l + (k,S)) -' (k,S) = l
let S be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: for l being Element of NAT holds (l + (k,S)) -' (k,S) = l
let l be Element of NAT ; :: thesis: (l + (k,S)) -' (k,S) = l
thus (l + (k,S)) -' (k,S) = il. (S,(((locnum (l,S)) + k) -' k)) by Def5
.= il. (S,(locnum (l,S))) by NAT_D:34
.= l by Def5 ; :: thesis: verum