let X be non empty set ; :: thesis: for Y being set
for S being SigmaField of X
for F being Function of NAT ,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 Function of NAT ,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 Function of NAT ,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 Function of NAT ,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_EAL (r + (1 / (n + 1))))) ;
then Y /\ (great_dom f,(R_EAL r)) = union (rng F) by MESFUNC1:26;
hence Y /\ (great_dom f,r) = union (rng F) ; :: thesis: verum