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 Function of NAT , bool REAL such that
A3:
for n being Element of NAT holds S1[n,GG . n]
from FUNCT_2:sch 3(A2);
GG is Interval_Covering of union (rng F)
proof
A4:
union (rng F) c= union (rng GG)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in union (rng F) or x in union (rng GG) )
assume
x in union (rng F)
;
:: thesis: x in union (rng GG)
then consider A being
set such that A5:
(
x in A &
A in rng F )
by TARSKI:def 4;
consider n1 being
set such that A6:
(
n1 in dom F &
A = F . n1 )
by A5, FUNCT_1:def 5;
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 A7:
(
x in AA &
AA in rng (G . n1) )
by A5, A6, TARSKI:def 4;
consider n2 being
set such that A8:
(
n2 in dom (G . n1) &
AA = (G . n1) . n2 )
by A7, FUNCT_1:def 5;
reconsider n2 =
n2 as
Element of
NAT by A8;
consider n being
set such that A9:
(
n in dom H &
[n1,n2] = H . n )
by A1, FUNCT_1:def 5;
reconsider n =
n as
Element of
NAT by A9;
[((pr1 H) . n),((pr2 H) . n)] = [n1,n2]
by A9, Def12;
then
(
(pr1 H) . n = n1 &
(pr2 H) . n = n2 )
by ZFMISC_1:33;
then
(
x in GG . n &
GG . n in rng GG )
by A3, A7, A8, FUNCT_2:6;
hence
x in union (rng GG)
by TARSKI:def 4;
:: thesis: verum
end;
for
n being
Element of
NAT holds
GG . n is
Interval
hence
GG is
Interval_Covering of
union (rng F)
by A4, Def2;
:: thesis: verum
end;
then reconsider GG = GG as Interval_Covering of union (rng F) ;
take
GG
; :: thesis: 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; :: thesis: verum