let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 Def18
.= leftker (RQForm f) by Th45
.= the carrier of (LKer (RQForm f)) by Def18 ;
hence LKer f = LKer (RQForm f) by VECTSP_4:29; :: thesis: verum