let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL holds
( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )
let f, g be PartFunc of X,REAL; :: thesis: ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )
dom ((R_EAL f) - (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC2:2;
then A1: dom ((R_EAL f) - (R_EAL g)) = dom (f - g) by VALUED_1:12;

A2: now :: thesis: for x being object st x in dom ((R_EAL f) - (R_EAL g)) holds
((R_EAL f) - (R_EAL g)) . x = (f - g) . x

let x be object ; :: thesis: ( x in dom ((R_EAL f) - (R_EAL g)) implies ((R_EAL f) - (R_EAL g)) . x = (f - g) . x )
assume A3: x in dom ((R_EAL f) - (R_EAL g)) ; :: thesis: ((R_EAL f) - (R_EAL g)) . x = (f - g) . x
then ((R_EAL f) - (R_EAL g)) . x = ((R_EAL f) . x) - ((R_EAL g) . x) by MESFUNC1:def 4
.= (f . x) - (g . x) by SUPINF_2:3 ;
hence ((R_EAL f) - (R_EAL g)) . x = (f - g) . x by A1, A3, VALUED_1:13; :: thesis: verum

end;

dom ((R_EAL f) + (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC2:2;
then A4: dom ((R_EAL f) + (R_EAL g)) = dom (f + g) by VALUED_1:def 1;

now :: thesis: for x being object st x in dom ((R_EAL f) + (R_EAL g)) holds
((R_EAL f) + (R_EAL g)) . x = (f + g) . x

let x be object ; :: thesis: ( x in dom ((R_EAL f) + (R_EAL g)) implies ((R_EAL f) + (R_EAL g)) . x = (f + g) . x )
assume A5: x in dom ((R_EAL f) + (R_EAL g)) ; :: thesis: ((R_EAL f) + (R_EAL g)) . x = (f + g) . x
then ((R_EAL f) + (R_EAL g)) . x = ((R_EAL f) . x) + ((R_EAL g) . x) by MESFUNC1:def 3
.= (f . x) + (g . x) by SUPINF_2:1 ;
hence ((R_EAL f) + (R_EAL g)) . x = (f + g) . x by A4, A5, VALUED_1:def 1; :: thesis: verum

end;

hence ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) ) by A4, A1, A2, FUNCT_1:2, MESFUNC2:2; :: thesis: verum