let X be RealUnitarySpace; :: thesis: for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)
let x, y, u, v be Point of X; :: thesis: (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)
(x - y) .|. (u - v) = (x .|. (u - v)) - (y .|. (u - v)) by Th11
.= ((x .|. u) - (x .|. v)) - (y .|. (u - v)) by Th12
.= ((x .|. u) - (x .|. v)) - ((y .|. u) - (y .|. v)) by Th12 ;
hence (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v) ; :: thesis: verum