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

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