per cases ( F₄() nin F₅() or F₄() in F₅() ) ;

suppose F₄() nin F₅() ; :: thesis: F₆() iteration_terminates_for F₂(),F₄()

hence F₆() iteration_terminates_for F₂(),F₄() by Th83; :: thesis: verum

end;

suppose A3: F₄() in F₅() ; :: thesis: F₆() iteration_terminates_for F₂(),F₄()

deffunc H₁( set , set ) -> Element of F₃() = F₆() . ((In ($2,F₃())),F₂());
consider f being sequence of F₃() such that
A4: f . 0 = F₄() and
A5: for i being Nat holds f . (i + 1) = H₁(i,f . i) from NAT_1:sch 12();
defpred S₁[ Nat] means ex i being Element of NAT st F₇((f . i)) = $1;
F₇((f . 0)) in NAT by ORDINAL1:def 12;
then A6: ex j being Nat st S₁[j] ;
consider j being Nat such that
A7: ( S₁[j] & ( for i being Nat st S₁[i] holds
j <= i ) ) from NAT_1:sch 5(A6);
consider i0 being Element of NAT such that
A8: F₇((f . i0)) = j by A7;
defpred S₂[ Nat] means P₁[f . $1];
In ((f . i0),F₃()) = f . i0 ;
then f . (i0 + 1) = F₆() . ((f . i0),F₂()) by A5;
then ( P₁[f . i0] implies F₇((f . (i0 + 1))) < j ) by A2, A8;
then A9: ex i being Nat st S₂[i] by A7;
consider j being Nat such that
A10: ( S₂[j] & ( for i being Nat st S₂[i] holds
j <= i ) ) from NAT_1:sch 5(A9);
deffunc H₂( Nat) -> Element of F₃() = f . ($1 -' 1);
consider p being FinSequence of F₃() such that
A11: ( len p = j + 1 & ( for i being Nat st i in dom p holds
p . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A12: dom p = Seg (j + 1) by A11, FINSEQ_1:def 3;
reconsider p = p as non empty FinSequence of F₃() by A11;
take p ; :: according to AOFA_000:def 33 :: thesis: ( p . 1 = F₄() & p . (len p) nin F₅() & ( for i being Nat st 1 <= i & i < len p holds
( p . i in F₅() & p . (i + 1) = F₆() . ((p . i),F₂()) ) ) )
A13: 1 <= j + 1 by NAT_1:11;
then 1 in Seg (j + 1) ;
hence p . 1 = H₂(1) by A11, A12
.= F₄() by A4, XREAL_1:232 ;
:: thesis: ( p . (len p) nin F₅() & ( for i being Nat st 1 <= i & i < len p holds
( p . i in F₅() & p . (i + 1) = F₆() . ((p . i),F₂()) ) ) )
len p in Seg (j + 1) by A11, A13;
then A14: p . (len p) = H₂(j + 1) by A11, A12
.= f . j by NAT_D:34 ;
j > 0 by A1, A3, A4, A10;
then j >= 0 + 1 by NAT_1:13;
then consider j9 being Nat such that
A15: j = 1 + j9 by NAT_1:10;
reconsider j9 = j9 as Element of NAT by ORDINAL1:def 12;
A16: f . j = F₆() . ((In ((f . j9),F₃())),F₂()) by A5, A15;
j9 < j by A15, NAT_1:13;
then P₁[f . j9] by A10;
hence p . (len p) nin F₅() by A2, A10, A14, A16; :: thesis: for i being Nat st 1 <= i & i < len p holds
( p . i in F₅() & p . (i + 1) = F₆() . ((p . i),F₂()) )
let i be Nat; :: thesis: ( 1 <= i & i < len p implies ( p . i in F₅() & p . (i + 1) = F₆() . ((p . i),F₂()) ) )
assume that
A18: 1 <= i and
A19: i < len p ; :: thesis: ( p . i in F₅() & p . (i + 1) = F₆() . ((p . i),F₂()) )
A20: i + 1 >= 1 by A18, NAT_1:13;
A21: i + 1 <= len p by A19, NAT_1:13;
A22: i in Seg (j + 1) by A11, A18, A19;
A23: i + 1 in Seg (j + 1) by A11, A20, A21;
A24: p . i = H₂(i) by A11, A12, A22;
A25: p . (i + 1) = H₂(i + 1) by A11, A12, A23;
consider i9 being Nat such that
A26: i = 1 + i9 by A18, NAT_1:10;
reconsider i9 = i9 as Element of NAT by ORDINAL1:def 12;
i <= j by A11, A19, NAT_1:13;
then A27: i9 < j by A26, NAT_1:13;
then A28: P₁[f . i9] by A10;
A29: i -' 1 = i9 by A26, NAT_D:34;
A30: (i + 1) -' 1 = i by NAT_D:34;
A31: In ((f . i9),F₃()) = f . i9 ;

now :: thesis: ( i9 <> 0 implies p . i in F₅() )

assume i9 <> 0 ; :: thesis: p . i in F₅()
then i9 >= 0 + 1 by NAT_1:13;
then consider i99 being Nat such that
A32: i9 = 1 + i99 by NAT_1:10;
reconsider i99 = i99 as Element of NAT by ORDINAL1:def 12;
i99 <= i9 by A32, NAT_1:11;
then i99 < j by A27, XXREAL_0:2;
then A33: P₁[f . i99] by A10;
f . i9 = H₁(i99,f . i99) by A5, A32;
hence p . i in F₅() by A2, A24, A28, A29, A33; :: thesis: verum

end;

hence ( p . i in F₅() & p . (i + 1) = F₆() . ((p . i),F₂()) ) by A3, A4, A5, A24, A25, A26, A29, A30, A31; :: thesis: verum

end;

end;