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