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

end;

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

end;