let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex ; for f being cmplxhomogeneousFAF Form of V,V
for v being Vector of V holds f . (v,(0. V)) = 0. F_Complex
let f be cmplxhomogeneousFAF Form of V,V; for v being Vector of V holds f . (v,(0. V)) = 0. F_Complex
let v be Vector of V; f . (v,(0. V)) = 0. F_Complex
set F = FunctionalFAF (f,v);
thus f . (v,(0. V)) =
f . (v,((0. F_Complex) * (0. V)))
by VECTSP10:1
.=
(FunctionalFAF (f,v)) . ((0. F_Complex) * (0. V))
by BILINEAR:8
.=
((0. F_Complex) *') * ((FunctionalFAF (f,v)) . (0. V))
by Def1
.=
0. F_Complex
by COMPLFLD:47
; verum