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) )
A1: ( dom (<>* (f + g)) = dom (f + g) & dom (<>* (f - g)) = dom (f - g) & dom (<>* f) = dom f & dom (<>* g) = dom g ) by Th3;
then ( dom (<>* (f + g)) = (dom (<>* f)) /\ (dom (<>* g)) & dom (<>* (f - g)) = (dom (<>* f)) /\ (dom (<>* g)) ) by VALUED_1:12, VALUED_1:def 1;
then A2: ( 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 object st x in dom (<>* (f + g)) holds
(<>* (f + g)) . x = ((<>* f) + (<>* g)) . x
let x be object ; :: thesis: ( x in dom (<>* (f + g)) implies (<>* (f + g)) . x = ((<>* f) + (<>* g)) . x )
assume A3: x in dom (<>* (f + g)) ; :: thesis: (<>* (f + g)) . x = ((<>* f) + (<>* g)) . x
then x in (dom f) /\ (dom g) by A1, 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 Th6;
(<>* (f + g)) . x = <*((f + g) . x)*> by Th6, A3, A1
.= <*((f . x) + (g . x))*> by A3, A1, VALUED_1:def 1
.= ((<>* f) . x) + ((<>* g) . x) by A4, RVSUM_1:13 ;
hence (<>* (f + g)) . x = ((<>* f) + (<>* g)) . x by A2, A3, VALUED_2:def 45; :: thesis: verum
end;
hence <>* (f + g) = (<>* f) + (<>* g) by A2, FUNCT_1:2; :: thesis: <>* (f - g) = (<>* f) - (<>* g)
now :: thesis: for x being object st x in dom (<>* (f - g)) holds
(<>* (f - g)) . x = ((<>* f) - (<>* g)) . x
let x be object ; :: thesis: ( x in dom (<>* (f - g)) implies (<>* (f - g)) . x = ((<>* f) - (<>* g)) . x )
assume A5: x in dom (<>* (f - g)) ; :: thesis: (<>* (f - g)) . x = ((<>* f) - (<>* g)) . x
then x in (dom f) /\ (dom g) by A1, VALUED_1:12;
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then A6: ( <*(f . x)*> = (<>* f) . x & <*(g . x)*> = (<>* g) . x ) by Th6;
thus (<>* (f - g)) . x = <*((f - g) . x)*> by Th6, A5, A1
.= <*((f . x) - (g . x))*> by A5, A1, VALUED_1:13
.= ((<>* f) . x) - ((<>* g) . x) by A6, RVSUM_1:29
.= ((<>* f) - (<>* g)) . x by A2, A5, VALUED_2:def 46 ; :: thesis: verum
end;
hence <>* (f - g) = (<>* f) - (<>* g) by A2, FUNCT_1:2; :: thesis: verum