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

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