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

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