let V be non empty VectSpStr of F_Complex ; :: thesis: for W being VectSp of
for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of
for w being Vector of holds (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
let W be VectSp of ; :: thesis: for f being additiveFAF cmplxhomogeneousFAF Form of V,W
for v being Vector of
for w being Vector of 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
for w being Vector of holds (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
let v be Vector of ; :: thesis: for w being Vector of holds (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
let w be Vector of ; :: thesis: (RQ*Form f) . v,(w + (RKer (f *' ))) = f . v,w
reconsider A = w + (RKer (f *' )) as Vector of 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