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,(I \; J)] in TerminatingPrograms (A,S,T,f)
let s be Element of S; :: thesis: for T being Subset of S
for f being ExecutionFunction of A,S,T holds [s,(I \; J)] in TerminatingPrograms (A,S,T,f)
let T be Subset of S; :: thesis: for f being ExecutionFunction of A,S,T holds [s,(I \; J)] in TerminatingPrograms (A,S,T,f)
let f be ExecutionFunction of A,S,T; :: thesis: [s,(I \; J)] in TerminatingPrograms (A,S,T,f)
A1: [s,I] in TerminatingPrograms (A,S,T,f) by Def36;
[(f . (s,I)),J] in TerminatingPrograms (A,S,T,f) by Def36;
hence [s,(I \; J)] in TerminatingPrograms (A,S,T,f) by A1, Def35; :: thesis: verum