let E be RealNormSpace; :: thesis: for a, b being Point of E holds ((a -reflection) . b) - a = a - b
let a, b be Point of E; :: thesis: ((a -reflection) . b) - a = a - b
set R = a -reflection ;
A1: 1 * a = a by RLVECT_1:def 8;
(a -reflection) . b = (2 * a) - b by Def4;
hence ((a -reflection) . b) - a = ((2 * a) - a) - b by VECTSP_1:34
.= ((2 - 1) * a) - b by A1, RLVECT_1:35
.= a - b by RLVECT_1:def 8 ;
:: thesis: verum