theorem Th97: :: AOFA_000:97

for A being preIfWhileAlgebra
for I, J being Element of A
for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(I \; J)] in TerminatingPrograms (A,S,T,f) holds
( [s,I] in TerminatingPrograms (A,S,T,f) & [(f . (s,I)),J] in TerminatingPrograms (A,S,T,f) )