set K = F_Complex ;
let V, W be VectSp of F_Complex ; :: thesis: for f being sesquilinear-Form of V,W holds RKer (f *') = RKer ((LQForm f) *')
let f be sesquilinear-Form of V,W; :: thesis: RKer (f *') = RKer ((LQForm f) *')
the carrier of (RKer (f *')) = rightker (f *') by BILINEAR:def 19
.= rightker f by Th55
.= rightker (LQForm f) by BILINEAR:44
.= rightker ((LQForm f) *') by Th55
.= the carrier of (RKer ((LQForm f) *')) by BILINEAR:def 19 ;
hence RKer (f *') = RKer ((LQForm f) *') by VECTSP_4:29; :: thesis: verum