let F be RFunctional of V; :: thesis: ( F is Real_homogeneous implies F is 0-preserving )
assume A1: F is Real_homogeneous ; :: thesis: F is 0-preserving
A2: 0. F_Complex = [**0 ,0 **] by COMPLFLD:9;
thus F . (0. V) = F . ((0. F_Complex ) * (0. V)) by VECTSP_1:59
.= 0 * (F . (0. V)) by A1, A2, Def18
.= 0 ; :: according to HAHNBAN1:def 20 :: thesis: verum