let V be RealLinearSpace; :: thesis: for x, y, u, v being VECTOR of V st Gen x,y holds
Ortm (x,y,(u - v)) = (Ortm (x,y,u)) - (Ortm (x,y,v))
let x, y, u, v be VECTOR of V; :: thesis: ( Gen x,y implies Ortm (x,y,(u - v)) = (Ortm (x,y,u)) - (Ortm (x,y,v)) )
assume A1: Gen x,y ; :: thesis: Ortm (x,y,(u - v)) = (Ortm (x,y,u)) - (Ortm (x,y,v))
hence Ortm (x,y,(u - v)) = (Ortm (x,y,u)) + (Ortm (x,y,(- v))) by Th1
.= (Ortm (x,y,u)) - (Ortm (x,y,v)) by A1, Th4 ;
:: thesis: verum