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 20
.= rightker f by Th58
.= rightker (LQForm f) by BILINEAR:45
.= rightker ((LQForm f) *' ) by Th58
.= the carrier of (RKer ((LQForm f) *' )) by BILINEAR:def 20 ;
hence RKer (f *' ) = RKer ((LQForm f) *' ) by VECTSP_4:37; :: thesis: verum