let F be FrFunctional of V; :: thesis: ( F is homogeneous implies F is 0-preserving )
assume A1: F is homogeneous ; :: thesis: F is 0-preserving
thus F . (0. V) = F . ((0. INT.Ring) * (0. V)) by VECTSP_1:14
.= (0. INT.Ring) * (F . (0. V)) by A1
.= 0. F_Real ; :: according to ZMODLAT1:def 31 :: thesis: verum