let r be Real; :: thesis: for f, g being Function of REAL,REAL holds r (#) (f +* g) = (r (#) f) +* (r (#) g)
let f, g be Function of REAL,REAL; :: thesis: r (#) (f +* g) = (r (#) f) +* (r (#) g)
set F1 = r (#) (f +* g);
set F2 = (r (#) f) +* (r (#) g);
D1: ( dom (r (#) (f +* g)) = REAL & dom ((r (#) f) +* (r (#) g)) = REAL ) by FUNCT_2:def 1;
for x being object st x in dom (r (#) (f +* g)) holds
(r (#) (f +* g)) . x = ((r (#) f) +* (r (#) g)) . x

proof

let x be object ; :: thesis: ( x in dom (r (#) (f +* g)) implies (r (#) (f +* g)) . x = ((r (#) f) +* (r (#) g)) . x )
assume A1: x in dom (r (#) (f +* g)) ; :: thesis: (r (#) (f +* g)) . x = ((r (#) f) +* (r (#) g)) . x
then reconsider x = x as Real ;
A2: x in REAL by A1;

per cases ( x in dom g or not x in dom g ) ;

suppose B1: x in dom g ; :: thesis: (r (#) (f +* g)) . x = ((r (#) f) +* (r (#) g)) . x

B2: x in dom (r (#) g) by FUNCT_2:def 1, A2;
(r (#) (f +* g)) . x = r * ((f +* g) . x) by VALUED_1:6
.= r * (g . x) by FUNCT_4:13, B1
.= (r (#) g) . x by VALUED_1:6
.= ((r (#) f) +* (r (#) g)) . x by FUNCT_4:13, B2 ;
hence (r (#) (f +* g)) . x = ((r (#) f) +* (r (#) g)) . x ; :: thesis: verum

end;

suppose C1: not x in dom g ; :: thesis: (r (#) (f +* g)) . x = ((r (#) f) +* (r (#) g)) . x

C2: dom g = REAL by FUNCT_2:def 1
.= dom (r (#) g) by FUNCT_2:def 1 ;
(r (#) (f +* g)) . x = r * ((f +* g) . x) by VALUED_1:6
.= r * (f . x) by FUNCT_4:11, C1
.= (r (#) f) . x by VALUED_1:6
.= ((r (#) f) +* (r (#) g)) . x by FUNCT_4:11, C2, C1 ;
hence (r (#) (f +* g)) . x = ((r (#) f) +* (r (#) g)) . x ; :: thesis: verum

end;

end;

end;

hence r (#) (f +* g) = (r (#) f) +* (r (#) g) by FUNCT_1:2, D1; :: thesis: verum