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

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