for p being set st p in BOOL F1() holds
p <> {} by ORDERS_1:1;
then consider Choice being Function such that
dom Choice = BOOL F1() and
A2: for p being set st p in BOOL F1() holds
Choice . p in p by FUNCT_1:111;
A3: F3() in F1() ;
ex g being sequence of F1() st
( g . 0 = F3() & ( for n being Element of NAT holds g . (n + 1) = Choice . ((F2() .: {(g . n)}) /\ F4((g . n))) ) )
proof
deffunc H1( object ) -> set = Choice . ((F2() .: {(k_id ($1,F1(),F3()))}) /\ F4((k_id ($1,F1(),F3()))));
A4: for x being object st x in F1() holds
H1(x) in F1()
proof
let x be object ; :: thesis: ( x in F1() implies H1(x) in F1() )
assume A5: x in F1() ; :: thesis: H1(x) in F1()
A6: k_id (x,F1(),F3()) = x by A5, Def1;
reconsider x = x as Element of F1() by A5;
set X = (Im (F2(),x)) /\ F4(x);
(Im (F2(),x)) /\ F4(x) is non empty Subset of F1() by A1;
then (Im (F2(),x)) /\ F4(x) in BOOL F1() by ORDERS_1:2;
then Choice . ((Im (F2(),x)) /\ F4(x)) in (Im (F2(),x)) /\ F4(x) by A2;
then A7: H1(x) in F2() .: {x} by A6, XBOOLE_0:def 4;
A8: rng F2() c= F1() by RELAT_1:def 19;
F2() .: {x} c= rng F2() by RELAT_1:111;
then F2() .: {x} c= F1() by A8;
hence H1(x) in F1() by A7; :: thesis: verum
end;
consider f being Function of F1(),F1() such that
A9: for x being object st x in F1() holds
f . x = H1(x) from FUNCT_2:sch 2(A4);
 deffunc H2( object ) -> Element of F1() = (f |** (k_nat $1)) . F3();
A10: for m being object st m in NAT holds
H2(m) in F1() ;
consider g being sequence of F1() such that
A11: for m being object st m in NAT holds
g . m = H2(m) from FUNCT_2:sch 2(A10);
 A12: for n being Element of NAT holds g . (n + 1) = Choice . ((F2() .: {(g . n)}) /\ F4((g . n)))
proof
let n be Element of NAT ; :: thesis: g . (n + 1) = Choice . ((F2() .: {(g . n)}) /\ F4((g . n)))
A13: F3() in dom (f |** n) by A3, FUNCT_2:def 1;
A14: k_id ((g . n),F1(),F3()) = g . n by Def1;
g . (n + 1) = H2(n + 1) by A11
.= (f |** (n + 1)) . F3() by Def2
.= (f * (f |** n)) . F3() by FUNCT_7:71
.= f . ((f |** n) . F3()) by A13, FUNCT_1:13
.= f . ((f |** (k_nat n)) . F3()) by Def2
.= f . (g . n) by A11
.= Choice . ((F2() .: {(g . n)}) /\ F4((g . n))) by A9, A14 ;
hence g . (n + 1) = Choice . ((F2() .: {(g . n)}) /\ F4((g . n))) ; :: thesis: verum
end;
take g ; :: thesis: ( g . 0 = F3() & ( for n being Element of NAT holds g . (n + 1) = Choice . ((F2() .: {(g . n)}) /\ F4((g . n))) ) )
g . 0 = H2( 0 ) by A11
.= (f |** 0) . F3() by Def2
.= (id F1()) . F3() by FUNCT_7:84
.= F3() ;
hence ( g . 0 = F3() & ( for n being Element of NAT holds g . (n + 1) = Choice . ((F2() .: {(g . n)}) /\ F4((g . n))) ) ) by A12; :: thesis: verum
end;
then consider g being sequence of F1() such that
A15: g . 0 = F3() and
A16: for n being Element of NAT holds g . (n + 1) = Choice . ((F2() .: {(g . n)}) /\ F4((g . n))) ;
take g ; :: thesis: ( g . 0 = F3() & ( for n being Element of NAT holds
( [(g . n),(g . (n + 1))] in F2() & g . (n + 1) in F4((g . n)) ) ) )
A17: for n being Element of NAT holds g . (n + 1) in (F2() .: {(g . n)}) /\ F4((g . n))
proof
let n be Element of NAT ; :: thesis: g . (n + 1) in (F2() .: {(g . n)}) /\ F4((g . n))
set s = g . n;
set X = (Im (F2(),(g . n))) /\ F4((g . n));
(Im (F2(),(g . n))) /\ F4((g . n)) is non empty Subset of F1() by A1;
then (Im (F2(),(g . n))) /\ F4((g . n)) in BOOL F1() by ORDERS_1:2;
then Choice . ((Im (F2(),(g . n))) /\ F4((g . n))) in (Im (F2(),(g . n))) /\ F4((g . n)) by A2;
hence g . (n + 1) in (F2() .: {(g . n)}) /\ F4((g . n)) by A16; :: thesis: verum
end;
for n being Element of NAT holds
( [(g . n),(g . (n + 1))] in F2() & g . (n + 1) in F4((g . n)) )
proof
let n be Element of NAT ; :: thesis: ( [(g . n),(g . (n + 1))] in F2() & g . (n + 1) in F4((g . n)) )
A18: g . (n + 1) in (Im (F2(),(g . n))) /\ F4((g . n)) by A17;
then g . (n + 1) in Im (F2(),(g . n)) by XBOOLE_0:def 4;
hence ( [(g . n),(g . (n + 1))] in F2() & g . (n + 1) in F4((g . n)) ) by A18, RELSET_2:9, XBOOLE_0:def 4; :: thesis: verum
end;
hence ( g . 0 = F3() & ( for n being Element of NAT holds
( [(g . n),(g . (n + 1))] in F2() & g . (n + 1) in F4((g . n)) ) ) ) by A15; :: thesis: verum