let V be RealLinearSpace; :: thesis: for u, x, y being VECTOR of V st Gen x,y holds

ex v being VECTOR of V st Orte (x,y,v) = u

let u, x, y be VECTOR of V; :: thesis: ( Gen x,y implies ex v being VECTOR of V st Orte (x,y,v) = u )

assume A1: Gen x,y ; :: thesis: ex v being VECTOR of V st Orte (x,y,v) = u

take v = - (Orte (x,y,u)); :: thesis: Orte (x,y,v) = u

thus Orte (x,y,v) = - (Orte (x,y,(Orte (x,y,u)))) by A1, Th9

.= - (- u) by A1, Th14

.= u by RLVECT_1:17 ; :: thesis: verum

ex v being VECTOR of V st Orte (x,y,v) = u

let u, x, y be VECTOR of V; :: thesis: ( Gen x,y implies ex v being VECTOR of V st Orte (x,y,v) = u )

assume A1: Gen x,y ; :: thesis: ex v being VECTOR of V st Orte (x,y,v) = u

take v = - (Orte (x,y,u)); :: thesis: Orte (x,y,v) = u

thus Orte (x,y,v) = - (Orte (x,y,(Orte (x,y,u)))) by A1, Th9

.= - (- u) by A1, Th14

.= u by RLVECT_1:17 ; :: thesis: verum