let E be RealNormSpace; :: thesis: for a, b being Point of E holds ||.(((a -reflection) . b) - a).|| = ||.(b - a).||
let a, b be Point of E; :: thesis: ||.(((a -reflection) . b) - a).|| = ||.(b - a).||
((a -reflection) . b) - a = a - b by Th19;
hence ||.(((a -reflection) . b) - a).|| = ||.(b - a).|| by NORMSP_1:7; :: thesis: verum