for E being RealNormSpace
for a, b being Point of E holds ((a -reflection) . b) - b = 2 * (a - b)