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