theorem RHS4: :: DUALSP04:2

for X being RealUnitarySpace
for x, y being Point of X
for x1, y1 being Point of (RUSp2RNSp X) st x = x1 & y = y1 holds
x - y = x1 - y1 by RHS3;