for A being preIfWhileAlgebra
for C, I being Element of A
for S being non empty set
for T being Subset of S
for f being Function of [:S, the carrier of A:],S st f is complying_with_empty-instruction & f complies_with_if_wrt T holds
for s being Element of S st f . (s,C) nin T holds
f . (s,(if-then (C,I))) = f . (s,C)