let V be VectSp of F_Complex ; for v, w being Vector of V
for f being sesquilinear-Form of V,V
for r being Real
for a being Element of F_Complex st |.a.| = 1 holds
f . ((v - (([**r,0**] * a) * w)),(v - (([**r,0**] * a) * w))) = (((f . (v,v)) - ([**r,0**] * (a * (f . (w,v))))) - ([**r,0**] * ((a *') * (f . (v,w))))) + ([**(r ^2),0**] * (f . (w,w)))
let v1, w be Vector of V; for f being sesquilinear-Form of V,V
for r being Real
for a being Element of F_Complex st |.a.| = 1 holds
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
let f be sesquilinear-Form of V,V; for r being Real
for a being Element of F_Complex st |.a.| = 1 holds
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
let r be Real; for a being Element of F_Complex st |.a.| = 1 holds
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
let a be Element of F_Complex; ( |.a.| = 1 implies f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w))) )
assume A1:
|.a.| = 1
; f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
set r1 = [**r,0**] * a;
set v3 = f . (v1,v1);
set v4 = f . (v1,w);
set w1 = f . (w,v1);
set w2 = f . (w,w);
A2: ([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w))) =
([**(r ^2),0**] * (a * (a *'))) * (f . (w,w))
.=
[**((r ^2) * (1 ^2)),0**] * (f . (w,w))
by A1, Th13
;
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) =
((f . (v1,v1)) - ((([**r,0**] * a) *') * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] * a) *') * (f . (w,w)))))
by Th38
.=
((f . (v1,v1)) - ((([**r,0**] *') * (a *')) * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] * a) *') * (f . (w,w)))))
by COMPLFLD:54
.=
((f . (v1,v1)) - (([**r,0**] * (a *')) * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] * a) *') * (f . (w,w)))))
by Th12, COMPLEX1:12
.=
((f . (v1,v1)) - (([**r,0**] * (a *')) * (f . (v1,w)))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * ((([**r,0**] *') * (a *')) * (f . (w,w)))))
by COMPLFLD:54
.=
((f . (v1,v1)) - ([**r,0**] * ((a *') * (f . (v1,w))))) - ((([**r,0**] * a) * (f . (w,v1))) - (([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w)))))
by Th12, COMPLEX1:12
.=
(((f . (v1,v1)) - ([**r,0**] * ((a *') * (f . (v1,w))))) - ([**r,0**] * (a * (f . (w,v1))))) + (([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w))))
by RLVECT_1:29
.=
(((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + (([**r,0**] * a) * (([**r,0**] * (a *')) * (f . (w,w))))
;
hence
f . ((v1 - (([**r,0**] * a) * w)),(v1 - (([**r,0**] * a) * w))) = (((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1))))) - ([**r,0**] * ((a *') * (f . (v1,w))))) + ([**(r ^2),0**] * (f . (w,w)))
by A2; verum