let n be Element of NAT ; :: thesis: for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal )
let x1, x2, y1 be Element of REAL n; :: thesis: ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal )

now

per cases ( x1 <> x2 or x1 = x2 ) ;

case A1: x1 <> x2 ; :: thesis: ( ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2) in Line x1,x2 & x1 - x2,y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2)) are_orthogonal )

set mu = - (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ));
set y2 = ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2);
|.(x1 - x2).| <> 0 by A1, Lm1;
then A2: |.(x1 - x2).| ^2 <> 0 by SQUARE_1:74;
|((x1 - x2),(y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2))))| = |((x1 - x2),((y1 - ((1 + (- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2)))| by RVSUM_1:60
.= |((x1 - x2),((y1 - ((1 * x1) + ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1))) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2)))| by EUCLID_4:7
.= |((x1 - x2),(((y1 - (1 * x1)) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2)))| by RVSUM_1:60
.= |((x1 - x2),(((y1 - x1) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2)))| by EUCLID_4:3
.= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2))))| by RVSUM_1:60
.= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + (- ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x2)))))| by Th8
.= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * (- x2)))))| by Th8
.= |((x1 - x2),((y1 - x1) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * (x1 - x2))))| by EUCLID_4:6
.= |((x1 - x2),(y1 - x1))| - |((x1 - x2),((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * (x1 - x2)))| by EUCLID_4:31
.= |((x1 - x2),(y1 - x1))| - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * |((x1 - x2),(x1 - x2))|) by EUCLID_4:26
.= |((x1 - x2),(y1 - x1))| + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * |((x1 - x2),(x1 - x2))|)
.= |((x1 - x2),(y1 - x1))| + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * (|.(x1 - x2).| ^2 )) by EUCLID_2:12
.= |((x1 - x2),(y1 - x1))| + (((- |((x1 - x2),(y1 - x1))|) / (|.(x1 - x2).| ^2 )) * (|.(x1 - x2).| ^2 )) by XCMPLX_1:188
.= |((x1 - x2),(y1 - x1))| + (- |((x1 - x2),(y1 - x1))|) by A2, XCMPLX_1:88
.= 0 ;
hence ( ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2) in Line x1,x2 & x1 - x2,y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 )))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2 ))) * x2)) are_orthogonal ) by RVSUM_1:def 18; :: thesis: verum

end;

case A3: x1 = x2 ; :: thesis: for mu being Real ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal )

let mu be Real; :: thesis: ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal )
set y2 = ((1 - mu) * x1) + (mu * x2);
take y2 = ((1 - mu) * x1) + (mu * x2); :: thesis: ( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal )
x1 - x2 = 0* n by A3, Th7;
then |((x1 - x2),(y1 - y2))| = 0 by EUCLID_4:23;
hence ( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal ) by RVSUM_1:def 18; :: thesis: verum

end;

end;

end;

hence ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal ) ; :: thesis: verum