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

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