let X be RealUnitarySpace; :: thesis: for M being Subspace of X
for x, m1, m2 being Point of X st m1 in M & m2 in M & ( for m being Point of X st m in M holds
||.(x - m1).|| <= ||.(x - m).|| ) & ( for m being Point of X st m in M holds
||.(x - m2).|| <= ||.(x - m).|| ) holds
m1 = m2
let M be Subspace of X; :: thesis: for x, m1, m2 being Point of X st m1 in M & m2 in M & ( for m being Point of X st m in M holds
||.(x - m1).|| <= ||.(x - m).|| ) & ( for m being Point of X st m in M holds
||.(x - m2).|| <= ||.(x - m).|| ) holds
m1 = m2
let x, m1, m2 be Point of X; :: thesis: ( m1 in M & m2 in M & ( for m being Point of X st m in M holds
||.(x - m1).|| <= ||.(x - m).|| ) & ( for m being Point of X st m in M holds
||.(x - m2).|| <= ||.(x - m).|| ) implies m1 = m2 )
assume that
A1: m1 in M and
A2: m2 in M and
A3: for m being Point of X st m in M holds
||.(x - m1).|| <= ||.(x - m).|| and
A4: for m being Point of X st m in M holds
||.(x - m2).|| <= ||.(x - m).|| ; :: thesis: m1 = m2
m1 - m2 in M by A1, A2, RUSUB_1:17;
then A5: (x - m1) .|. (m1 - m2) = 0 by Lm2, A3, A1;
A6: (x - m1) + (m1 - m2) = ((x - m1) + m1) - m2 by RLVECT_1:28
.= x - m2 by RLVECT_4:1 ;
assume m1 <> m2 ; :: thesis: contradiction
then m1 - m2 <> 0. X by RLVECT_1:21;
then ||.(m1 - m2).|| <> 0 by BHSP_1:26;
then (||.(x - m1).|| ^2) + 0 < (||.(x - m1).|| ^2) + (||.(m1 - m2).|| ^2) by XREAL_1:8, SQUARE_1:12;
then A7: ||.(x - m1).|| ^2 < ||.(x - m2).|| ^2 by A6, BHSP_5:6, BHSP_1:def 3, A5;
0 <= ||.(x - m2).|| by BHSP_1:28;
hence contradiction by A7, SQUARE_1:15, A1, A4; :: thesis: verum