:: deftheorem Def29 defines complying_with_catenation AOFA_000:def 29 :
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_catenation iff for s being Element of S
for I1, I2 being Element of A holds f . (s,(I1 \; I2)) = f . ((f . (s,I1)),I2) );