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

hereby :: according to HAHNBAN:def 4 :: 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:13
.= (f . x) + 0 by FUNCOP_1:13
.= (f . x) + (f . y) by FUNCOP_1:13 ; :: thesis: verum

end;

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

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

end;

let x be VECTOR of V; :: according to HAHNBAN:def 5 :: 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:13
.= r * (f . x) by FUNCOP_1:13 ; :: thesis: verum