let S be non empty set ; :: according to AOFA_000:def 36 :: thesis: for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f
thus for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms A,S,T,f by Th96; :: thesis: verum