let f1 be PartFunc of REAL , REAL ; :: thesis: for n, m being Element of REAL holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1
let n, m be Element of REAL ; :: thesis: (n (#) f1) + (m (#) f1) = (n + m) (#) f1
B1: 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 ;
B2: dom ((n (#) f1) + (m (#) f1)) = dom ((n + m) (#) f1) by B1, VALUED_1:def 5;
for x being Real st x in dom f1 holds
((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x

proof

let x be Real; :: thesis: ( x in dom f1 implies ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x )
assume A2: x in dom f1 ; :: thesis: ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x
B4: x in dom (n (#) f1) by A2, VALUED_1:def 5;
B5: x in dom (m (#) f1) by A2, VALUED_1:def 5;
A4: ((n (#) f1) + (m (#) f1)) . x = ((n (#) f1) . x) + ((m (#) f1) . x) by A2, B1, VALUED_1:def 1
.= (n * (f1 . x)) + ((m (#) f1) . x) by B4, VALUED_1:def 5
.= (n * (f1 . x)) + (m * (f1 . x)) by B5, VALUED_1:def 5 ;
x in dom ((n + m) (#) f1) by A2, VALUED_1:def 5;
then ((n + m) (#) f1) . x = (n + m) * (f1 . x) by VALUED_1:def 5
.= (n * (f1 . x)) + (m * (f1 . x)) ;
hence ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x by A4; :: thesis: verum

end;

hence (n (#) f1) + (m (#) f1) = (n + m) (#) f1 by B1, B2, PARTFUN1:34; :: thesis: verum