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 number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v)) = |.(f . w,v).| & Im (a * (f . w,v)) = 0 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 number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 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 number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 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 number ; :: thesis: for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 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 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 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 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 ) ; :: 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 v3 = f . v1,v1;
set v4 = f . v1,w;
set w1 = f . w,v1;
set w2 = f . w,w;
set r1 = [**r,0 **] * a;
A2: Im [**r,0 **] = 0 by COMPLEX1:28;
A3: 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 Th41
.= ((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:90
.= ((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 A2, Th14
.= ((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:90
.= ((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 A2, Th14
.= (((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:43
.= (((f . v1,v1) - ([**r,0 **] * (a * (f . w,v1)))) - ([**r,0 **] * ((a *' ) * (f . v1,w)))) + (([**r,0 **] * a) * (([**r,0 **] * (a *' )) * (f . w,w))) ;
([**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, Th16 ;
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 A3; :: thesis: verum