let V be VectSp of F_Complex ; for v, w being Vector of V
for f being hermitan-Form of V holds (((f . v,w) + (f . v,w)) + (f . v,w)) + (f . v,w) = (((f . (v + w),(v + w)) - (f . (v - w),(v - w))) + (i_FC * (f . (v + (i_FC * w)),(v + (i_FC * w))))) - (i_FC * (f . (v - (i_FC * w)),(v - (i_FC * w))))
let v1, w be Vector of V; for f being hermitan-Form of V holds (((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w) = (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w))))
let f be hermitan-Form of V; (((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w) = (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w))))
set v3 = f . v1,v1;
set v4 = f . v1,w;
set w2 = f . w,w;
set w1 = f . w,v1;
( f . (v1 + w),(v1 + w) = ((f . v1,v1) + (f . v1,w)) + ((f . w,v1) + (f . w,w)) & f . (v1 - w),(v1 - w) = ((f . v1,v1) - (f . v1,w)) - ((f . w,v1) - (f . w,w)) )
by Th39, BILINEAR:29;
then A1: (f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w)) =
(((f . v1,v1) + (f . v1,w)) - (((f . v1,v1) - (f . v1,w)) - ((f . w,v1) - (f . w,w)))) + ((f . w,v1) + (f . w,w))
.=
((((f . v1,v1) + (f . v1,w)) - ((f . v1,v1) - (f . v1,w))) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w))
by RLVECT_1:43
.=
((((f . v1,v1) - ((f . v1,v1) - (f . v1,w))) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w))
.=
(((((f . v1,v1) - (f . v1,v1)) + (f . v1,w)) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w))
by RLVECT_1:43
.=
((((0. F_Complex ) + (f . v1,w)) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w))
by RLVECT_1:28
.=
(((f . v1,w) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w))
by RLVECT_1:def 7
.=
((f . v1,w) + (f . v1,w)) + ((((f . w,v1) - (f . w,w)) + (f . w,w)) + (f . w,v1))
.=
((f . v1,w) + (f . v1,w)) + (((f . w,v1) - ((f . w,w) - (f . w,w))) + (f . w,v1))
by RLVECT_1:43
.=
((f . v1,w) + (f . v1,w)) + (((f . w,v1) - (0. F_Complex )) + (f . w,v1))
by RLVECT_1:28
.=
((f . v1,w) + (f . v1,w)) + ((f . w,v1) + (f . w,v1))
by RLVECT_1:26
;
f . (v1 + (i_FC * w)),(v1 + (i_FC * w)) =
((f . v1,v1) + ((i_FC *' ) * (f . v1,w))) + ((i_FC * (f . w,v1)) + (i_FC * ((i_FC *' ) * (f . w,w))))
by Th40
.=
((f . v1,v1) + ((i_FC *' ) * (f . v1,w))) + (i_FC * ((f . w,v1) + ((i_FC *' ) * (f . w,w))))
;
then A2: i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))) =
(i_FC * ((f . v1,v1) + ((i_FC *' ) * (f . v1,w)))) + ((i_FC * i_FC ) * ((f . w,v1) + ((i_FC *' ) * (f . w,w))))
.=
((i_FC * (f . v1,v1)) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))
by COMPLEX1:17, HAHNBAN1:8, VECTSP_6:81
;
f . (v1 - (i_FC * w)),(v1 - (i_FC * w)) =
(f . v1,(v1 - (i_FC * w))) - (f . (i_FC * w),(v1 - (i_FC * w)))
by BILINEAR:36
.=
((f . v1,v1) - (f . v1,(i_FC * w))) - (f . (i_FC * w),(v1 - (i_FC * w)))
by Th38
.=
((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (f . (i_FC * w),(v1 - (i_FC * w)))
by Th30
.=
((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (i_FC * (f . w,(v1 - (i_FC * w))))
by BILINEAR:32
.=
((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (i_FC * ((f . w,v1) - (f . w,(i_FC * w))))
by Th38
.=
((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (i_FC * ((f . w,v1) - ((i_FC *' ) * (f . w,w))))
by Th30
;
then i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w))) =
(i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) - (i_FC * (i_FC * ((f . w,v1) - ((i_FC *' ) * (f . w,w)))))
by VECTSP_1:43
.=
(i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) - ((i_FC * i_FC ) * ((f . w,v1) - ((i_FC *' ) * (f . w,w))))
.=
(i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) - (- ((f . w,v1) - ((i_FC *' ) * (f . w,w))))
by HAHNBAN1:8, VECTSP_6:81
.=
(i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) + ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
by COMPLFLD:35
.=
((i_FC * (f . v1,v1)) - (i_FC * ((i_FC *' ) * (f . v1,w)))) + ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
by VECTSP_1:43
.=
((i_FC * (f . v1,v1)) - (f . v1,w)) + ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
by COMPLEX1:17
;
then (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w)))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w)))) =
((((i_FC * (f . v1,v1)) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((i_FC * (f . v1,v1)) - (f . v1,w))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
by A2, RLVECT_1:41
.=
((((i_FC * (f . v1,v1)) + (f . v1,w)) - ((i_FC * (f . v1,v1)) - (f . v1,w))) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
.=
(((((f . v1,w) + (i_FC * (f . v1,v1))) - (i_FC * (f . v1,v1))) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
by RLVECT_1:43
.=
((((f . v1,w) + ((i_FC * (f . v1,v1)) - (i_FC * (f . v1,v1)))) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
.=
((((f . v1,w) + (0. F_Complex )) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
by RLVECT_1:28
.=
(((f . v1,w) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
by RLVECT_1:def 7
.=
((f . v1,w) + (f . v1,w)) - (((f . w,v1) + ((i_FC *' ) * (f . w,w))) + ((f . w,v1) - ((i_FC *' ) * (f . w,w))))
by RLVECT_1:41
.=
((f . v1,w) + (f . v1,w)) - (((f . w,v1) + (f . w,v1)) + (((i_FC *' ) * (f . w,w)) - ((i_FC *' ) * (f . w,w))))
.=
((f . v1,w) + (f . v1,w)) - (((f . w,v1) + (f . w,v1)) + (0. F_Complex ))
by RLVECT_1:28
.=
((f . v1,w) + (f . v1,w)) - ((f . w,v1) + (f . w,v1))
by RLVECT_1:def 7
;
then (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w)))) =
((f . v1,w) + (f . v1,w)) + ((((f . w,v1) + (f . w,v1)) + ((f . v1,w) + (f . v1,w))) - ((f . w,v1) + (f . w,v1)))
by A1
.=
((f . v1,w) + (f . v1,w)) + ((f . v1,w) + (f . v1,w))
by COMPLFLD:41
.=
(((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w)
;
hence
(((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w) = (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w))))
; verum