let A be preIfWhileAlgebra; :: thesis:
let S be non empty set ; :: thesis:
let T be Subset of S; :: thesis:
let s be Element of S; :: thesis:
let f be ExecutionFunction of A,S,T; :: thesis:
let C, I be Element of A; :: thesis:
assume that
A1: C is_terminating_wrt f and
A2: I is_terminating_wrt f ; :: thesis:
given r being non empty FinSequence of S such that A3: r . 1 = f . (s,C) and
A4: r . (len r) nin T and
A5: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),(I \; C)) ) ; :: according to AOFA_000:def 33 :: thesis:

let i be Nat; :: thesis:
assume that
A7: 1 <= i and
A8: i < len r ; :: thesis:
thus r . i in T by A5, A7, A8; :: thesis:
then reconsider s = r . i as Element of S ;
A9: [s,I] in TerminatingPrograms (A,S,T,f) by A2;
[(f . (s,I)),C] in TerminatingPrograms (A,S,T,f) by A1;
hence ( [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) by A5, A7, A8, A9, Def35; :: thesis:

end;