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

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