let X be set ; for S being SigmaField of X
for F being sequence of S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,n)) ) holds
A /\ (eq_dom (f,+infty)) = meet (rng F)
let S be SigmaField of X; for F being sequence of S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,n)) ) holds
A /\ (eq_dom (f,+infty)) = meet (rng F)
let F be sequence of S; for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,n)) ) holds
A /\ (eq_dom (f,+infty)) = meet (rng F)
let f be PartFunc of X,ExtREAL; for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,n)) ) holds
A /\ (eq_dom (f,+infty)) = meet (rng F)
let A be set ; ( ( for n being Element of NAT holds F . n = A /\ (great_dom (f,n)) ) implies A /\ (eq_dom (f,+infty)) = meet (rng F) )
assume A1:
for n being Element of NAT holds F . n = A /\ (great_dom (f,n))
; A /\ (eq_dom (f,+infty)) = meet (rng F)
for x being object st x in A /\ (eq_dom (f,+infty)) holds
x in meet (rng F)
then A8:
A /\ (eq_dom (f,+infty)) c= meet (rng F)
;
for x being object st x in meet (rng F) holds
x in A /\ (eq_dom (f,+infty))
then
meet (rng F) c= A /\ (eq_dom (f,+infty))
;
hence
A /\ (eq_dom (f,+infty)) = meet (rng F)
by A8, XBOOLE_0:def 10; verum