let F be sequence of (bool REAL); :: thesis: for G being Open_Interval_Covering of F
for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds
On (G,H) is Open_Interval_Covering of union (rng F)
let G be Open_Interval_Covering of F; :: thesis: for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds
On (G,H) is Open_Interval_Covering of union (rng F)
let H be sequence of [:NAT,NAT:]; :: thesis: ( rng H = [:NAT,NAT:] implies On (G,H) is Open_Interval_Covering of union (rng F) )
assume A1: rng H = [:NAT,NAT:] ; :: thesis: On (G,H) is Open_Interval_Covering of union (rng F)
for n being Element of NAT holds (On (G,H)) . n is open_interval
proof
let n be Element of NAT ; :: thesis: (On (G,H)) . n is open_interval
(On (G,H)) . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A1, MEASURE7:def 11;
hence (On (G,H)) . n is open_interval ; :: thesis: verum
end;
hence On (G,H) is Open_Interval_Covering of union (rng F) by Def5; :: thesis: verum