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:43
.= (((2 * a) - (2 * a)) - b) + c by VECTSP_1:93
.= ((0. E) - b) + c by RLVECT_1:28
.= c - b by RLVECT_1:27 ;
hence ||.(((a -reflection) . b) - ((a -reflection) . c)).|| = ||.(b - c).|| by NORMSP_1:11; :: thesis: verum