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 RKer f = RKer (LQForm f)
let V, W be VectSp of K; :: thesis: for f being bilinear-Form of V,W holds RKer f = RKer (LQForm f)
let f be bilinear-Form of V,W; :: thesis: RKer f = RKer (LQForm f)
the carrier of (RKer f) = rightker f by Def19
.= rightker (LQForm f) by Th44
.= the carrier of (RKer (LQForm f)) by Def19 ;
hence RKer f = RKer (LQForm f) by VECTSP_4:29; :: thesis: verum