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