let f be Functional of V; :: thesis: ( f is additive implies f is subadditive )
assume A1: f is additive ; :: thesis: f is subadditive
let x, y be VECTOR of V; :: according to HAHNBAN:def 1 :: thesis: f . (x + y) <= (f . x) + (f . y)
thus f . (x + y) <= (f . x) + (f . y) by A1, Def4; :: thesis: verum