reconsider f = the carrier of V --> (In (0,REAL)) as Functional of V ;
take f ; :: thesis: ( f is additive & f is absolutely_homogeneous & f is homogeneous )

hereby :: according to HAHNBAN:def 2 :: thesis: ( f is absolutely_homogeneous & f is homogeneous )

let x, y be VECTOR of V; :: thesis: f . (x + y) = (f . x) + (f . y)
thus f . (x + y) = 0 + 0 by FUNCOP_1:7
.= (f . x) + 0 by FUNCOP_1:7
.= (f . x) + (f . y) by FUNCOP_1:7 ; :: thesis: verum

end;

hereby :: according to HAHNBAN:def 6 :: thesis: f is homogeneous

let x be VECTOR of V; :: thesis: for r being Real holds f . (r * x) = |.r.| * (f . x)
let r be Real; :: thesis: f . (r * x) = |.r.| * (f . x)
thus f . (r * x) = |.r.| * 0 by FUNCOP_1:7
.= |.r.| * (f . x) by FUNCOP_1:7 ; :: thesis: verum

end;

let x be VECTOR of V; :: according to HAHNBAN:def 3 :: thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; :: thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = r * 0 by FUNCOP_1:7
.= r * (f . x) by FUNCOP_1:7 ; :: thesis: verum