A1: now :: thesis:

assume f iteration_terminates_for I,s ; :: thesis:
then consider r being non empty FinSequence of S such that
A2: r . 1 = s and
A3: r . (len r) nin T and
A4: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) ) ;
reconsider x = (len r) - 1 as R_eal by XXREAL_0:def 1;
take x = x; :: thesis:
take r = r; :: thesis:
thus ( x = (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 A2, A3, A4; :: thesis:

end;

now :: thesis:

let d1, d2 be R_eal; :: thesis:
given r1 being non empty FinSequence of S such that A5: d1 = (len r1) - 1 and
A6: r1 . 1 = s and
A7: r1 . (len r1) nin T and
A8: for i being Nat st 1 <= i & i < len r1 holds
( r1 . i in T & r1 . (i + 1) = f . ((r1 . i),I) ) ; :: thesis:
given r2 being non empty FinSequence of S such that A9: d2 = (len r2) - 1 and
A10: r2 . 1 = s and
A11: r2 . (len r2) nin T and
A12: for i being Nat st 1 <= i & i < len r2 holds
( r2 . i in T & r2 . (i + 1) = f . ((r2 . i),I) ) ; :: thesis:
defpred S₁[ Nat] means ( $1 < len r1 implies ( $1 < len r2 & r1 . ($1 + 1) = r2 . ($1 + 1) ) );
A13: S₁[ 0 ] by A6, A10;

A14: now :: thesis:

let i be Nat; :: thesis:
assume A15: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

proof

assume A16: i + 1 < len r1 ; :: thesis:
A17: 1 <= i + 1 by NAT_1:11;
then A18: r1 . ((i + 1) + 1) = f . ((r1 . (i + 1)),I) by A8, A16;
A19: r1 . (i + 1) in T by A8, A16, A17;
i + 1 <= len r2 by A15, A16, NAT_1:13;
hence i + 1 < len r2 by A11, A15, A16, A19, NAT_1:13, XXREAL_0:1; :: thesis:
hence r1 . ((i + 1) + 1) = r2 . ((i + 1) + 1) by A12, A15, A16, A17, A18, NAT_1:13; :: thesis:

end;

end;

A20: for i being Nat holds S₁[i] from NAT_1:sch 2(A13, A14);
consider i being Nat such that
A21: len r1 = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i < len r1 by A21, NAT_1:13;
then A22: r1 . (len r1) = r2 . (len r1) by A20, A21;
A23: 1 <= len r1 by A21, NAT_1:11;
A24: len r1 <= len r2 by A20;
len r2 <= len r1 by A7, A12, A22, A23;
hence d1 = d2 by A5, A9, A24, XXREAL_0:1; :: thesis:

end;

hence ( ( for b₁ being R_eal holds verum ) & ( f iteration_terminates_for I,s implies ex b₁ being R_eal ex r being non empty FinSequence of S st
( b₁ = (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) ) ) ) ) & ( not f iteration_terminates_for I,s implies ex b₁ being R_eal st b₁ = +infty ) & ( for b₁, b₂ being R_eal holds
( ( f iteration_terminates_for I,s & ex r being non empty FinSequence of S st
( b₁ = (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) ) ) ) & ex r being non empty FinSequence of S st
( b₂ = (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) ) ) ) implies b₁ = b₂ ) & ( not f iteration_terminates_for I,s & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) ) ) ) by A1; :: thesis: