let A be preIfWhileAlgebra; :: thesis: for I being Element of A
for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree I,s,f < +infty )
let I be Element of A; :: thesis: for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree I,s,f < +infty )
let S be non empty set ; :: thesis: for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree I,s,f < +infty )
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree I,s,f < +infty )
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff iteration-degree I,s,f < +infty )
let f be ExecutionFunction of A,S,T; :: thesis: ( f iteration_terminates_for I,s iff iteration-degree I,s,f < +infty )

hereby :: thesis: ( iteration-degree I,s,f < +infty implies f iteration_terminates_for I,s )

assume f iteration_terminates_for I,s ; :: thesis: iteration-degree I,s,f < +infty
then consider r being non empty FinSequence of S such that
A1: ( iteration-degree I,s,f = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . (r . i),I ) ) ) by Def34;
(len r) - 1 in REAL by XREAL_0:def 1;
hence iteration-degree I,s,f < +infty by A1, XXREAL_0:9; :: thesis: verum

end;

thus ( iteration-degree I,s,f < +infty implies f iteration_terminates_for I,s ) by Def34; :: thesis: verum