let V be RealLinearSpace; :: thesis: for x, y, u being VECTOR of V st Gen x,y holds
Ortm x,y,(Ortm x,y,u) = u
let x, y, u 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