let f be Function of (REAL m),(REAL n); :: thesis: ( f = (REAL m) --> (0* n) implies ( f is additive & f is homogeneous ) )
assume A1: f = (REAL m) --> (0* n) ; :: thesis: ( f is additive & f is homogeneous )
reconsider n1 = n as Nat ;

hereby :: according to PDIFF_6:def 1 :: thesis: f is homogeneous

let x, y be Element of REAL m; :: thesis: f . (x + y) = (f . x) + (f . y)
A2: 0. (REAL-NS n1) = 0* n by REAL_NS1:def 4;
f . (x + y) = 0* n by A1, FUNCOP_1:7
.= 0. (REAL-NS n1) by REAL_NS1:def 4
.= (0. (REAL-NS n1)) + (0. (REAL-NS n1)) by RLVECT_1:4
.= (0* n) + (0* n) by A2, REAL_NS1:2
.= (f . x) + (0* n) by A1, FUNCOP_1:7 ;
hence f . (x + y) = (f . x) + (f . y) by A1, FUNCOP_1:7; :: thesis: verum

end;

hereby :: according to PDIFF_6:def 2 :: thesis: verum

let x be Element of REAL m; :: thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; :: thesis: f . (r * x) = r * (f . x)
A3: 0. (REAL-NS n1) = 0* n by REAL_NS1:def 4;
f . (r * x) = 0* n by A1, FUNCOP_1:7
.= 0. (REAL-NS n1) by REAL_NS1:def 4
.= r * (0. (REAL-NS n1)) by RLVECT_1:10
.= r * (0* n) by A3, REAL_NS1:3 ;
hence f . (r * x) = r * (f . x) by A1, FUNCOP_1:7; :: thesis: verum

end;