let E be RealNormSpace; :: thesis: for a, b being Point of E holds ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).||
let a, b be Point of E; :: thesis: ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).||
A1: ((a -reflection) . b) - b = 2 * (a - b) by Th21;
A2: |.2.| = 2 by COMPLEX1:43;
||.(a - b).|| = ||.(b - a).|| by NORMSP_1:7;
hence ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).|| by A1, A2, NORMSP_1:def 1; :: thesis: verum