let V be VectSp of F_Complex ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( |.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 ; :: thesis: 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; :: thesis: verum