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 A1: 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)
A2: (R_EAL f) + (R_EAL g) = R_EAL (f + g) by Th23;
for p being Rational holds F . p = (A /\ (less_dom (R_EAL f),(R_EAL p))) /\ (A /\ (less_dom (R_EAL g),(R_EAL (r - p)))) by A1;
then A /\ (less_dom ((R_EAL f) + (R_EAL g)),(R_EAL r)) = union (rng F) by MESFUNC2:3;
hence A /\ (less_dom (f + g),r) = union (rng F) by A2; :: thesis: verum