let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex ; :: thesis: 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; :: thesis: for v being Vector of V holds f . (v,(0. V)) = 0. F_Complex
let v be Vector of V; :: thesis: 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 ; :: thesis: verum