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 Th36, BILINEAR:28;
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:29
.=
((((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:29
.=
((((0. F_Complex) + (f . (v1,w))) + (f . (v1,w))) + ((f . (w,v1)) - (f . (w,w)))) + ((f . (w,v1)) + (f . (w,w)))
by RLVECT_1:15
.=
(((f . (v1,w)) + (f . (v1,w))) + ((f . (w,v1)) - (f . (w,w)))) + ((f . (w,v1)) + (f . (w,w)))
by RLVECT_1:def 4
.=
((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:29
.=
((f . (v1,w)) + (f . (v1,w))) + (((f . (w,v1)) - (0. F_Complex)) + (f . (w,v1)))
by RLVECT_1:15
.=
((f . (v1,w)) + (f . (v1,w))) + ((f . (w,v1)) + (f . (w,v1)))
by RLVECT_1:13
;
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 Th37
.=
((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:7, HAHNBAN1:4, VECTSP_6:48
;
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:35
.=
((f . (v1,v1)) - (f . (v1,(i_FC * w)))) - (f . ((i_FC * w),(v1 - (i_FC * w))))
by Th35
.=
((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (f . ((i_FC * w),(v1 - (i_FC * w))))
by Th27
.=
((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (i_FC * (f . (w,(v1 - (i_FC * w)))))
by BILINEAR:31
.=
((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (i_FC * ((f . (w,v1)) - (f . (w,(i_FC * w)))))
by Th35
.=
((f . (v1,v1)) - ((i_FC *') * (f . (v1,w)))) - (i_FC * ((f . (w,v1)) - ((i_FC *') * (f . (w,w)))))
by Th27
;
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:11
.=
(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:4, VECTSP_6:48
.=
(i_FC * ((f . (v1,v1)) - ((i_FC *') * (f . (v1,w))))) + ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))
by COMPLFLD:11
.=
((i_FC * (f . (v1,v1))) - (i_FC * ((i_FC *') * (f . (v1,w))))) + ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))
by VECTSP_1:11
.=
((i_FC * (f . (v1,v1))) - (f . (v1,w))) + ((f . (w,v1)) - ((i_FC *') * (f . (w,w))))
by COMPLEX1:7
;
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:27
.=
((((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:29
.=
((((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:15
.=
(((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 4
.=
((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:27
.=
((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:15
.=
((f . (v1,w)) + (f . (v1,w))) - ((f . (w,v1)) + (f . (w,v1)))
by RLVECT_1:def 4
;
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:12
.=
(((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