let x, y, z be Element of COMPLEX ; :: thesis: ( x <> y & z <> y & ( angle x,y,z = PI / 2 or angle x,y,z = (3 / 2) * PI ) implies (|.(x - y).| ^2 ) + (|.(z - y).| ^2 ) = |.(x - z).| ^2 )
assume A1: ( x <> y & z <> y & ( angle x,y,z = PI / 2 or angle x,y,z = (3 / 2) * PI ) ) ; :: thesis: (|.(x - y).| ^2 ) + (|.(z - y).| ^2 ) = |.(x - z).| ^2
A2: (|.(x - y).| ^2 ) + (|.(z - y).| ^2 ) = (Re ((x - y) .|. (x - y))) + (|.(z - y).| ^2 ) by Th44
.= (Re ((x - y) .|. (x - y))) + (Re ((z - y) .|. (z - y))) by Th44
.= Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) by COMPLEX1:19 ;
set x3 = x - z;
x - z = (x - y) - (z - y) ;
then (x - z) .|. (x - z) = ((((x - y) .|. (x - y)) - ((x - y) .|. (z - y))) - ((z - y) .|. (x - y))) + ((z - y) .|. (z - y)) by Th63;
then Re ((x - z) .|. (x - z)) = Re ((((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) - (((x - y) .|. (z - y)) + ((z - y) .|. (x - y))))
.= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (Re (((x - y) .|. (z - y)) + ((z - y) .|. (x - y)))) by COMPLEX1:48
.= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re ((z - y) .|. (x - y)))) by COMPLEX1:19
.= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re (((x - y) .|. (z - y)) *' ))) by Th47
.= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re ((x - y) .|. (z - y)))) by COMPLEX1:112
.= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (0 + (Re ((x - y) .|. (z - y)))) by A1, Lm4
.= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - 0 by A1, Lm4
.= Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) ;
hence (|.(x - y).| ^2 ) + (|.(z - y).| ^2 ) = |.(x - z).| ^2 by A2, Th44; :: thesis: verum