set R = a -reflection ;
let b be Point of E; :: according to MAZURULM:def 1 :: thesis: for b being Point of E holds ||.(((a -reflection) . b) - ((a -reflection) . b)).|| = ||.(b - b).||
let c be Point of E; :: thesis: ||.(((a -reflection) . b) - ((a -reflection) . c)).|| = ||.(b - c).||
( (a -reflection) . b = (2 * a) - b & (a -reflection) . c = (2 * a) - c ) by Def4;
then ((a -reflection) . b) - ((a -reflection) . c) = (((2 * a) - b) - (2 * a)) + c by RLVECT_1:29
.= (((2 * a) - (2 * a)) - b) + c by VECTSP_1:34
.= ((0. E) - b) + c by RLVECT_1:15
.= c - b ;
hence ||.(((a -reflection) . b) - ((a -reflection) . c)).|| = ||.(b - c).|| by NORMSP_1:7; :: thesis: verum