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

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