for p being set st p in BOOL F₁() holds
p <> {} by ORDERS_1:1;
then consider Choice being Function such that
dom Choice = BOOL F₁() and
A2: for p being set st p in BOOL F₁() holds
Choice . p in p by FUNCT_1:111;
A3: F₃() in F₁() ;
ex g being sequence of F₁() st
( g . 0 = F₃() & ( for n being Element of NAT holds g . (n + 1) = Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n))) ) )

proof

deffunc H₁( object ) -> set = Choice . ((F₂() .: {(k_id ($1,F₁(),F₃()))}) /\ F₄((k_id ($1,F₁(),F₃()))));
A4: for x being object st x in F₁() holds
H₁(x) in F₁()

proof

let x be object ; :: thesis: ( x in F₁() implies H₁(x) in F₁() )
assume A5: x in F₁() ; :: thesis: H₁(x) in F₁()
A6: k_id (x,F₁(),F₃()) = x by A5, Def1;
reconsider x = x as Element of F₁() by A5;
set X = (Im (F₂(),x)) /\ F₄(x);
(Im (F₂(),x)) /\ F₄(x) is non empty Subset of F₁() by A1;
then (Im (F₂(),x)) /\ F₄(x) in BOOL F₁() by ORDERS_1:2;
then Choice . ((Im (F₂(),x)) /\ F₄(x)) in (Im (F₂(),x)) /\ F₄(x) by A2;
then A7: H₁(x) in F₂() .: {x} by A6, XBOOLE_0:def 4;
A8: rng F₂() c= F₁() by RELAT_1:def 19;
F₂() .: {x} c= rng F₂() by RELAT_1:111;
then F₂() .: {x} c= F₁() by A8;
hence H₁(x) in F₁() by A7; :: thesis: verum

end;

consider f being Function of F₁(),F₁() such that
A9: for x being object st x in F₁() holds
f . x = H₁(x) from FUNCT_2:sch 2(A4);
deffunc H₂( object ) -> Element of F₁() = (f |** (k_nat $1)) . F₃();
A10: for m being object st m in NAT holds
H₂(m) in F₁() ;
consider g being sequence of F₁() such that
A11: for m being object st m in NAT holds
g . m = H₂(m) from FUNCT_2:sch 2(A10);
A12: for n being Element of NAT holds g . (n + 1) = Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n)))

proof

let n be Element of NAT ; :: thesis: g . (n + 1) = Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n)))
A13: F₃() in dom (f |** n) by A3, FUNCT_2:def 1;
A14: k_id ((g . n),F₁(),F₃()) = g . n by Def1;
g . (n + 1) = H₂(n + 1) by A11
.= (f |** (n + 1)) . F₃() by Def2
.= (f * (f |** n)) . F₃() by FUNCT_7:71
.= f . ((f |** n) . F₃()) by A13, FUNCT_1:13
.= f . ((f |** (k_nat n)) . F₃()) by Def2
.= f . (g . n) by A11
.= Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n))) by A9, A14 ;
hence g . (n + 1) = Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n))) ; :: thesis: verum

end;

take g ; :: thesis: ( g . 0 = F₃() & ( for n being Element of NAT holds g . (n + 1) = Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n))) ) )
g . 0 = H₂( 0 ) by A11
.= (f |** 0) . F₃() by Def2
.= (id F₁()) . F₃() by FUNCT_7:84
.= F₃() ;
hence ( g . 0 = F₃() & ( for n being Element of NAT holds g . (n + 1) = Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n))) ) ) by A12; :: thesis: verum

end;

then consider g being sequence of F₁() such that
A15: g . 0 = F₃() and
A16: for n being Element of NAT holds g . (n + 1) = Choice . ((F₂() .: {(g . n)}) /\ F₄((g . n))) ;
take g ; :: thesis: ( g . 0 = F₃() & ( for n being Element of NAT holds
( [(g . n),(g . (n + 1))] in F₂() & g . (n + 1) in F₄((g . n)) ) ) )
A17: for n being Element of NAT holds g . (n + 1) in (F₂() .: {(g . n)}) /\ F₄((g . n))

proof

let n be Element of NAT ; :: thesis: g . (n + 1) in (F₂() .: {(g . n)}) /\ F₄((g . n))
set s = g . n;
set X = (Im (F₂(),(g . n))) /\ F₄((g . n));
(Im (F₂(),(g . n))) /\ F₄((g . n)) is non empty Subset of F₁() by A1;
then (Im (F₂(),(g . n))) /\ F₄((g . n)) in BOOL F₁() by ORDERS_1:2;
then Choice . ((Im (F₂(),(g . n))) /\ F₄((g . n))) in (Im (F₂(),(g . n))) /\ F₄((g . n)) by A2;
hence g . (n + 1) in (F₂() .: {(g . n)}) /\ F₄((g . n)) by A16; :: thesis: verum

end;

for n being Element of NAT holds
( [(g . n),(g . (n + 1))] in F₂() & g . (n + 1) in F₄((g . n)) )

proof

let n be Element of NAT ; :: thesis: ( [(g . n),(g . (n + 1))] in F₂() & g . (n + 1) in F₄((g . n)) )
A18: g . (n + 1) in (Im (F₂(),(g . n))) /\ F₄((g . n)) by A17;
then g . (n + 1) in Im (F₂(),(g . n)) by XBOOLE_0:def 4;
hence ( [(g . n),(g . (n + 1))] in F₂() & g . (n + 1) in F₄((g . n)) ) by A18, RELSET_2:9, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( g . 0 = F₃() & ( for n being Element of NAT holds
( [(g . n),(g . (n + 1))] in F₂() & g . (n + 1) in F₄((g . n)) ) ) ) by A15; :: thesis: verum