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

proof

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

end;

N is subadditive

proof

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

end;

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