let X be non empty set ; 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 /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let Y be 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 /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let S be 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 /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let F be sequence of S; for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let f be PartFunc of X,REAL; for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let r be Real; ( ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) implies Y /\ (less_eq_dom (f,r)) = meet (rng F) )
assume
for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1)))))
; Y /\ (less_eq_dom (f,r)) = meet (rng F)
then
for n being Element of NAT holds F . n = Y /\ (less_dom ((R_EAL f),(r + (1 / (n + 1)))))
;
then
Y /\ (less_eq_dom (f,r)) = meet (rng F)
by MESFUNC1:20;
hence
Y /\ (less_eq_dom (f,r)) = meet (rng F)
; verum