let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let f, g be PartFunc of X,REAL; :: thesis: for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let A be Element of S; :: thesis: for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let r be Real; :: thesis: for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let F be Function of RAT,S; :: thesis: ( ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) implies A /\ (less_dom ((f + g),r)) = union (rng F) )
assume for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; :: thesis: A /\ (less_dom ((f + g),r)) = union (rng F)
then for p being Rational holds F . p = (A /\ (less_dom ((R_EAL f),p))) /\ (A /\ (less_dom ((R_EAL g),(r - p)))) ;
then A1: A /\ (less_dom (((R_EAL f) + (R_EAL g)),r)) = union (rng F) by MESFUNC2:3;
(R_EAL f) + (R_EAL g) = R_EAL (f + g) by Th23;
hence A /\ (less_dom ((f + g),r)) = union (rng F) by A1; :: thesis: verum