for z being Nat
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 P being NAT -defined the InstructionsF of b₃ -valued finite lower Function holds
( z < card P iff il. (T,z) in dom P )