let V be non empty right_complementable add-associative right_zeroed VectSp-like VectSpStr of 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:2
.= (FunctionalFAF f,v) . ((0. F_Complex ) * (0. V)) by BILINEAR:9
.= ((0. F_Complex ) *' ) * ((FunctionalFAF f,v) . (0. V)) by Def1
.= 0. F_Complex by COMPLFLD:83, VECTSP_1:36 ; :: thesis: verum