let X be non empty set ; :: thesis: for Y being set
for S being SigmaField of X
for F being sequence of S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let Y be set ; :: thesis: for S being SigmaField of X
for F being sequence of S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let S be SigmaField of X; :: thesis: for F being sequence of S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let F be sequence of S; :: thesis: for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let f be PartFunc of X,REAL; :: thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let r be Real; :: thesis: ( ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) implies Y /\ (great_dom (f,r)) = union (rng F) )
assume for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ; :: thesis: Y /\ (great_dom (f,r)) = union (rng F)
then for n being Element of NAT holds F . n = Y /\ (great_eq_dom ((R_EAL f),(r + (1 / (n + 1))))) ;
then Y /\ (great_dom (f,r)) = union (rng F) by MESFUNC1:22;
hence Y /\ (great_dom (f,r)) = union (rng F) ; :: thesis: verum