let V be non empty ModuleStr over 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:23;
thus (RQ*Form f) . (v,(w + (RKer (f *')))) = ((RQForm (f *')) . (v,A)) *' by Def8
.= ((f *') . (v,w)) *' by BILINEAR:def 21
.= ((f . (v,w)) *') *' by Def8
.= f . (v,w) ; :: thesis: verum