:: deftheorem Def12 defines with_if-instruction AOFA_000:def 12 :
for S being non empty UAStr holds
( S is with_if-instruction iff ( 3 in dom the charact of S & the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S ) );