defpred S1[ Element of NAT , Subset of REAL] means $2 = (G . ((pr1 H) . $1)) . ((pr2 H) . $1);
A1:
for n being Element of NAT ex y being Subset of REAL st S1[n,y]
;
consider GG being Function of NAT,(bool REAL) such that
A2:
for n being Element of NAT holds S1[n,GG . n]
from FUNCT_2:sch 3(A1);
A3:
union (rng F) c= union (rng GG)
proof
let x be
set ;
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 A4:
x in A
and A5:
A in rng F
by TARSKI:def 4;
consider n1 being
set such that A6:
n1 in dom F
and A7:
A = F . n1
by A5, FUNCT_1:def 3;
reconsider n1 =
n1 as
Element of
NAT by A6;
F . n1 c= union (rng (G . n1))
by Def2;
then consider AA being
set such that A8:
x in AA
and A9:
AA in rng (G . n1)
by A4, A7, TARSKI:def 4;
consider n2 being
set such that A10:
n2 in dom (G . n1)
and A11:
AA = (G . n1) . n2
by A9, FUNCT_1:def 3;
reconsider n2 =
n2 as
Element of
NAT by A10;
consider n being
set such that A12:
n in dom H
and A13:
[n1,n2] = H . n
by B1, FUNCT_1:def 3;
reconsider n =
n as
Element of
NAT by A12;
[((pr1 H) . n),((pr2 H) . n)] = [n1,n2]
by A13, FUNCT_2:119;
then
(
(pr1 H) . n = n1 &
(pr2 H) . n = n2 )
by XTUPLE_0:1;
then A14:
x in GG . n
by A2, A8, A11;
GG . n in rng GG
by FUNCT_2:4;
hence
x in union (rng GG)
by A14, 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 A3, 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 A2; verum