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 u = Ortm x,y,v
let x, y, u 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