for S being non empty set
for T being Subset of S
for A being free ECIW-strict preIfWhileAlgebra
for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds
TerminatingPrograms (A,S,T,f1) = TerminatingPrograms (A,S,T,f2)