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

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