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