set K = F_Complex ;
let V, W be VectSp of F_Complex ; :: thesis: for f being sesquilinear-Form of V,W holds LKer f = LKer (RQ*Form f)
let f be sesquilinear-Form of V,W; :: thesis: LKer f = LKer (RQ*Form f)
the carrier of (LKer f) = leftker f by BILINEAR:def 18
.= leftker (RQ*Form f) by Th60
.= the carrier of (LKer (RQ*Form f)) by BILINEAR:def 18 ;
hence LKer f = LKer (RQ*Form f) by VECTSP_4:29; :: thesis: verum