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 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 Def20
.= rightker (LQForm f) by Th45
.= the carrier of (RKer (LQForm f)) by Def20 ;
hence RKer f = RKer (LQForm f) by VECTSP_4:29; :: thesis: verum