let V be RealLinearSpace; :: thesis: for x, y, u being VECTOR of V st Gen x,y holds
ex v being VECTOR of V st Orte x,y,v = u
let x, y, u 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:30 ; :: thesis: verum