:: deftheorem Def10 defines with_empty-instruction AOFA_000:def 10 :
for S being non empty UAStr holds
( S is with_empty-instruction iff ( 1 in dom the charact of S & the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S ) );