theorem Th32: :: AMI_WSTD:32

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 being NAT -defined the InstructionsF of b₂ -valued non empty finite lower Function holds LastLoc F = il. (T,((card F) -' 1))