theorem :: AOFA_000:117

for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds
while (C,I) is_terminating_wrt f