let E be RealNormSpace; :: thesis: for a, b being Point of E holds ((a -reflection) . b) - b = 2 * (a - b)
let a, b be Point of E; :: thesis: ((a -reflection) . b) - b = 2 * (a - b)
((2 * a) - b) - b = (2 * a) - (b + b) by RLVECT_1:27
.= (2 * a) - (2 * b) by Th3
.= 2 * (a - b) by RLVECT_1:34 ;
hence ((a -reflection) . b) - b = 2 * (a - b) by Def4; :: thesis: verum