let F be RFunctional 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 HAHNBAN1:def 16 :: thesis: F . (x + y) <= (F . x) + (F . y)
thus F . (x + y) <= (F . x) + (F . y) by A1, Def17; :: thesis: verum