let f be Functional 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. K) * (0. V)) by Th2
.= (0. K) * (f . (0. V)) by A1, HAHNBAN1:def 12
.= 0. K by VECTSP_1:39 ; :: according to HAHNBAN1:def 13 :: thesis: verum