let V be non empty VectSpStr of F_Complex ; :: thesis: for W being VectSp of F_Complex
for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of V
for w being Vector of W holds (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
let W be VectSp of F_Complex ; :: thesis: for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of V
for w being Vector of W holds (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
let f be additiveFAF cmplxhomogeneousFAF Form of V,W; :: thesis: for v being Vector of V
for w being Vector of W holds (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
let v be Vector of V; :: thesis: for w being Vector of W holds (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
let w be Vector of W; :: thesis: (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
reconsider A = w + (RKer (f *' )) as Vector of (VectQuot W,(RKer (f *' ))) by VECTSP10:24;
thus (RQ*Form f) . v,(w + (RKer (f *' ))) = ((RQForm (f *' )) . v,A) *' by Def8
.= ((f *' ) . v,w) *' by BILINEAR:def 22
.= ((f . v,w) *' ) *' by Def8
.= f . v,w ; :: thesis: verum