let V be RealNormSpace; :: thesis: the normF of V is subadditive absolutely_homogeneous Functional of V
reconsider N = the normF of V as Functional of V ;
A1: N is subadditive

proof

let x, y be VECTOR of V; :: according to HAHNBAN:def 1 :: thesis: N . (x + y) <= (N . x) + (N . y)
A2: N . (x + y) = ||.(x + y).|| by NORMSP_0:def 1;
( N . x = ||.x.|| & N . y = ||.y.|| ) by NORMSP_0:def 1;
hence N . (x + y) <= (N . x) + (N . y) by A2, NORMSP_1:def 1; :: thesis: verum

end;

N is absolutely_homogeneous

proof

let x be VECTOR of V; :: according to HAHNBAN:def 6 :: thesis: for r being Real holds N . (r * x) = |.r.| * (N . x)
let r be Real; :: thesis: N . (r * x) = |.r.| * (N . x)
thus N . (r * x) = ||.(r * x).|| by NORMSP_0:def 1
.= |.r.| * ||.x.|| by NORMSP_1:def 1
.= |.r.| * (N . x) by NORMSP_0:def 1 ; :: thesis: verum

end;

hence the normF of V is subadditive absolutely_homogeneous Functional of V by A1; :: thesis: verum