let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V holds LKer f = RKer (f *' )
let f be diagReR+0valued hermitan-Form of V; :: thesis: LKer f = RKer (f *' )
the carrier of (LKer f) = leftker f by BILINEAR:def 19
.= diagker f by Th55
.= rightker f by Th56
.= rightker (f *' ) by Th58
.= the carrier of (RKer (f *' )) by BILINEAR:def 20 ;
hence LKer f = RKer (f *' ) by VECTSP_4:37; :: thesis: verum