theorem Th23: :: AMI_WSTD:23

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 F being NAT -defined the InstructionsF of b₂ -valued finite Function st F is really-closed & il. (S,0) in dom F holds
F is para-closed by AMISTD_1:14;