let i be Element of NAT ; :: thesis: for f, g being PartFunc of (REAL i),REAL holds
( <>* (f + g) = (<>* f) + (<>* g) & <>* (f - g) = (<>* f) - (<>* g) )
let f, g be PartFunc of (REAL i),REAL; :: thesis: ( <>* (f + g) = (<>* f) + (<>* g) & <>* (f - g) = (<>* f) - (<>* g) )
P1: ( dom (<>* (f + g)) = dom (f + g) & dom (<>* (f - g)) = dom (f - g) & dom (<>* f) = dom f & dom (<>* g) = dom g ) by LMXTh0;
then ( dom (<>* (f + g)) = (dom (<>* f)) /\ (dom (<>* g)) & dom (<>* (f - g)) = (dom (<>* f)) /\ (dom (<>* g)) ) by VALUED_1:12, VALUED_1:def 1;
then P4: ( dom (<>* (f + g)) = dom ((<>* f) + (<>* g)) & dom (<>* (f - g)) = dom ((<>* f) - (<>* g)) ) by VALUED_2:def 45, VALUED_2:def 46;

now :: thesis: for x being set st x in dom (<>* (f + g)) holds
(<>* (f + g)) . x = ((<>* f) + (<>* g)) . x

let x be set ; :: thesis: ( x in dom (<>* (f + g)) implies (<>* (f + g)) . x = ((<>* f) + (<>* g)) . x )
assume A0: x in dom (<>* (f + g)) ; :: thesis: (<>* (f + g)) . x = ((<>* f) + (<>* g)) . x
then x in (dom f) /\ (dom g) by P1, VALUED_1:def 1;
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then A4: ( <*(f . x)*> = (<>* f) . x & <*(g . x)*> = (<>* g) . x ) by XTh30;
(<>* (f + g)) . x = <*((f + g) . x)*> by XTh30, A0, P1
.= <*((f . x) + (g . x))*> by A0, P1, VALUED_1:def 1
.= ((<>* f) . x) + ((<>* g) . x) by A4, RVSUM_1:13 ;
hence (<>* (f + g)) . x = ((<>* f) + (<>* g)) . x by P4, A0, VALUED_2:def 45; :: thesis: verum

end;

hence <>* (f + g) = (<>* f) + (<>* g) by P4, FUNCT_1:2; :: thesis: <>* (f - g) = (<>* f) - (<>* g)

now :: thesis: for x being set st x in dom (<>* (f - g)) holds
(<>* (f - g)) . x = ((<>* f) - (<>* g)) . x

let x be set ; :: thesis: ( x in dom (<>* (f - g)) implies (<>* (f - g)) . x = ((<>* f) - (<>* g)) . x )
assume A0: x in dom (<>* (f - g)) ; :: thesis: (<>* (f - g)) . x = ((<>* f) - (<>* g)) . x
then x in (dom f) /\ (dom g) by P1, VALUED_1:12;
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then A4: ( <*(f . x)*> = (<>* f) . x & <*(g . x)*> = (<>* g) . x ) by XTh30;
thus (<>* (f - g)) . x = <*((f - g) . x)*> by XTh30, A0, P1
.= <*((f . x) - (g . x))*> by A0, P1, VALUED_1:13
.= ((<>* f) . x) - ((<>* g) . x) by A4, RVSUM_1:29
.= ((<>* f) - (<>* g)) . x by P4, A0, VALUED_2:def 46 ; :: thesis: verum

end;

hence <>* (f - g) = (<>* f) - (<>* g) by P4, FUNCT_1:2; :: thesis: verum