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 18
.= diagker f by Th52
.= rightker f by Th53
.= rightker (f *') by Th55
.= the carrier of (RKer (f *')) by BILINEAR:def 19 ;
hence LKer f = RKer (f *') by VECTSP_4:29; :: thesis: verum