let V be RealLinearSpace; :: thesis: for x, y, u, v being VECTOR of V st Gen x,y & Ortm x,y,u = Ortm x,y,v holds
u = v
let x, y, u, v 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:28;
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:41;
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 6;
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 6;
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:49;
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:49;
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