defpred S1[ Element of NAT , Subset of REAL] means $2 = (G . ((pr1 H) . $1)) . ((pr2 H) . $1);
A2:
for n being Element of NAT ex y being Subset of REAL st S1[n,y]
;
consider GG being sequence of (bool REAL) such that
A3:
for n being Element of NAT holds S1[n,GG . n]
from FUNCT_2:sch 3(A2);
A4:
union (rng F) c= union (rng GG)
proof
let x be
object ;
TARSKI:def 3 ( not x in union (rng F) or x in union (rng GG) )
assume
x in union (rng F)
;
x in union (rng GG)
then consider A being
set such that A5:
x in A
and A6:
A in rng F
by TARSKI:def 4;
consider n1 being
object such that A7:
n1 in dom F
and A8:
A = F . n1
by A6, FUNCT_1:def 3;
reconsider n1 =
n1 as
Element of
NAT by A7;
F . n1 c= union (rng (G . n1))
by Def2;
then consider AA being
set such that A9:
x in AA
and A10:
AA in rng (G . n1)
by A5, A8, TARSKI:def 4;
consider n2 being
object such that A11:
n2 in dom (G . n1)
and A12:
AA = (G . n1) . n2
by A10, FUNCT_1:def 3;
reconsider n2 =
n2 as
Element of
NAT by A11;
consider n being
object such that A13:
n in dom H
and A14:
[n1,n2] = H . n
by A1, FUNCT_1:def 3;
reconsider n =
n as
Element of
NAT by A13;
[((pr1 H) . n),((pr2 H) . n)] = [n1,n2]
by A14, FUNCT_2:119;
then
(
(pr1 H) . n = n1 &
(pr2 H) . n = n2 )
by XTUPLE_0:1;
then A15:
x in GG . n
by A3, A9, A12;
GG . n in rng GG
by FUNCT_2:4;
hence
x in union (rng GG)
by A15, TARSKI:def 4;
verum
end;
for n being Element of NAT holds GG . n is Interval
then reconsider GG = GG as Interval_Covering of union (rng F) by A4, Def2;
take
GG
; for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)
thus
for n being Element of NAT holds GG . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)
by A3; verum