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 u = Ortm (x,y,v)
let u, x, y be VECTOR of V; :: thesis: ( Gen x,y implies ex v being VECTOR of V st u = Ortm (x,y,v) )
assume A1: Gen x,y ; :: thesis: ex v being VECTOR of V st u = Ortm (x,y,v)
take Ortm (x,y,u) ; :: thesis: u = Ortm (x,y,(Ortm (x,y,u)))
thus u = Ortm (x,y,(Ortm (x,y,u))) by A1, Th7; :: thesis: verum