let V be RealLinearSpace; :: thesis: for u, v, x, y being VECTOR of V st Gen x,y & Ortm (x,y,u) = Ortm (x,y,v) holds
u = v
let u, v, x, y be VECTOR of V; :: thesis: ( Gen x,y & Ortm (x,y,u) = Ortm (x,y,v) implies u = v )
assume that
A1: Gen x,y and
A2: Ortm (x,y,u) = Ortm (x,y,v) ; :: thesis: u = v
(((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y)) - (((pr1 (x,y,v)) * x) + ((- (pr2 (x,y,v))) * y)) = 0. V by A2, RLVECT_1:15;
then ((((pr1 (x,y,u)) * x) + ((- (pr2 (x,y,u))) * y)) - ((pr1 (x,y,v)) * x)) - ((- (pr2 (x,y,v))) * y) = 0. V by RLVECT_1:27;
then ((((pr1 (x,y,u)) * x) + (- ((pr1 (x,y,v)) * x))) + ((- (pr2 (x,y,u))) * y)) - ((- (pr2 (x,y,v))) * y) = 0. V by RLVECT_1:def 3;
then (((pr1 (x,y,u)) * x) - ((pr1 (x,y,v)) * x)) + (((- (pr2 (x,y,u))) * y) - ((- (pr2 (x,y,v))) * y)) = 0. V by RLVECT_1:def 3;
then (((pr1 (x,y,u)) - (pr1 (x,y,v))) * x) + (((- (pr2 (x,y,u))) * y) - ((- (pr2 (x,y,v))) * y)) = 0. V by RLVECT_1:35;
then A3: (((pr1 (x,y,u)) - (pr1 (x,y,v))) * x) + (((- (pr2 (x,y,u))) - (- (pr2 (x,y,v)))) * y) = 0. V by RLVECT_1:35;
then A4: (pr1 (x,y,u)) - (pr1 (x,y,v)) = 0 by A1, ANALMETR:def 1;
(- (pr2 (x,y,u))) - (- (pr2 (x,y,v))) = 0 by A1, A3, ANALMETR:def 1;
hence u = ((pr1 (x,y,v)) * x) + ((pr2 (x,y,v)) * y) by A1, A4, Lm5
.= v by A1, Lm5 ;
:: thesis: verum