let F be Functional of V; :: thesis: ( F is cmplxhomogeneous implies F is 0-preserving )

assume A1: F is cmplxhomogeneous ; :: thesis: F is 0-preserving

thus F . (0. V) = F . ((0. F_Complex) * (0. V)) by VECTSP10:1

.= ((0. F_Complex) *') * (F . (0. V)) by A1

.= 0. F_Complex by COMPLFLD:47 ; :: according to HAHNBAN1:def 9 :: thesis: verum

assume A1: F is cmplxhomogeneous ; :: thesis: F is 0-preserving

thus F . (0. V) = F . ((0. F_Complex) * (0. V)) by VECTSP10:1

.= ((0. F_Complex) *') * (F . (0. V)) by A1

.= 0. F_Complex by COMPLFLD:47 ; :: according to HAHNBAN1:def 9 :: thesis: verum