let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V, W being VectSp of K
for f being bilinear-Form of V,W holds LKer f = LKer (RQForm f)
let V, W be VectSp of K; :: thesis: for f being bilinear-Form of V,W holds LKer f = LKer (RQForm f)
let f be bilinear-Form of V,W; :: thesis: LKer f = LKer (RQForm f)
the carrier of (LKer f) = leftker f by Def19
.= leftker (RQForm f) by Th46
.= the carrier of (LKer (RQForm f)) by Def19 ;
hence LKer f = LKer (RQForm f) by VECTSP_4:37; :: thesis: verum