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

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