let V be RealLinearSpace; :: thesis: for u, x, y being VECTOR of V st Gen x,y holds
Orte (x,y,(Orte (x,y,u))) = - u
let u, x, y be VECTOR of V; :: thesis: ( Gen x,y implies Orte (x,y,(Orte (x,y,u))) = - u )
assume A1: Gen x,y ; :: thesis: Orte (x,y,(Orte (x,y,u))) = - u
hence Orte (x,y,(Orte (x,y,u))) = ((- (pr1 (x,y,u))) * x) + ((- (pr1 (x,y,(((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y))))) * y) by GEOMTRAP:def 5
.= ((- (pr1 (x,y,u))) * x) + ((- (pr2 (x,y,u))) * y) by A1, GEOMTRAP:def 4
.= ((pr1 (x,y,u)) * (- x)) + ((- (pr2 (x,y,u))) * y) by RLVECT_1:24
.= (- ((pr1 (x,y,u)) * x)) + ((- (pr2 (x,y,u))) * y) by RLVECT_1:25
.= (- ((pr1 (x,y,u)) * x)) + ((pr2 (x,y,u)) * (- y)) by RLVECT_1:24
.= (- ((pr1 (x,y,u)) * x)) + (- ((pr2 (x,y,u)) * y)) by RLVECT_1:25
.= - (((pr1 (x,y,u)) * x) + ((pr2 (x,y,u)) * y)) by RLVECT_1:31
.= - u by A1, Lm5 ;
:: thesis: verum