:: deftheorem Def28 defines complying_with_empty-instruction AOFA_000:def 28 :
for A being preIfWhileAlgebra
for S being non empty set
for f being Function of [:S, the carrier of A:],S holds
( f is complying_with_empty-instruction iff for s being Element of S holds f . (s,(EmptyIns A)) = s );