let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for l being Element of NAT holds l -' 0 ,S = l
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for l being Element of NAT holds l -' 0 ,S = l
let l be Element of NAT ; :: thesis: l -' 0 ,S = l
thus l -' 0 ,S = il. S,(locnum l,S) by NAT_D:40
.= l by Def13 ; :: thesis: verum