let f1 be PartFunc of REAL,REAL; :: thesis: for n, m being Real holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1
let n, m be Real; :: thesis: (n (#) f1) + (m (#) f1) = (n + m) (#) f1
A1: dom ((n (#) f1) + (m (#) f1)) = (dom (n (#) f1)) /\ (dom (m (#) f1)) by VALUED_1:def 1
.= (dom f1) /\ (dom (m (#) f1)) by VALUED_1:def 5
.= (dom f1) /\ (dom f1) by VALUED_1:def 5
.= dom f1 ;
A2: for x being Element of REAL st x in dom f1 holds
((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom f1 implies ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x )
assume A3: x in dom f1 ; :: thesis: ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x
then A4: x in dom (n (#) f1) by VALUED_1:def 5;
x in dom ((n + m) (#) f1) by A3, VALUED_1:def 5;
then A5: ((n + m) (#) f1) . x = (n + m) * (f1 . x) by VALUED_1:def 5
.= (n * (f1 . x)) + (m * (f1 . x)) ;
A6: x in dom (m (#) f1) by A3, VALUED_1:def 5;
((n (#) f1) + (m (#) f1)) . x = ((n (#) f1) . x) + ((m (#) f1) . x) by A1, A3, VALUED_1:def 1
.= (n * (f1 . x)) + ((m (#) f1) . x) by A4, VALUED_1:def 5
.= (n * (f1 . x)) + (m * (f1 . x)) by A6, VALUED_1:def 5 ;
hence ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x by A5; :: thesis: verum

end;

dom ((n (#) f1) + (m (#) f1)) = dom ((n + m) (#) f1) by A1, VALUED_1:def 5;
hence (n (#) f1) + (m (#) f1) = (n + m) (#) f1 by A1, A2, PARTFUN1:5; :: thesis: verum