let E be RealNormSpace; :: thesis: for a being Point of E holds

( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds

a = b ) )

let a be Point of E; :: thesis: ( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds

a = b ) )

set R = a -reflection ;

thus (a -reflection) . a = (2 * a) - a by Def4

.= (a + a) - a by Th3

.= a + (a - a) by RLVECT_1:28

.= a + (0. E) by RLVECT_1:15

.= a ; :: thesis: for b being Point of E st (a -reflection) . b = b holds

a = b

let b be Point of E; :: thesis: ( (a -reflection) . b = b implies a = b )

assume (a -reflection) . b = b ; :: thesis: a = b

then A1: ((a -reflection) . b) + b = 2 * b by Th3;

(a -reflection) . b = (2 * a) - b by Def4;

then ((a -reflection) . b) + b = (2 * a) - (b - b) by RLVECT_1:29

.= (2 * a) - (0. E) by RLVECT_1:15

.= 2 * a ;

hence a = b by A1, RLVECT_1:36; :: thesis: verum

( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds

a = b ) )

let a be Point of E; :: thesis: ( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds

a = b ) )

set R = a -reflection ;

thus (a -reflection) . a = (2 * a) - a by Def4

.= (a + a) - a by Th3

.= a + (a - a) by RLVECT_1:28

.= a + (0. E) by RLVECT_1:15

.= a ; :: thesis: for b being Point of E st (a -reflection) . b = b holds

a = b

let b be Point of E; :: thesis: ( (a -reflection) . b = b implies a = b )

assume (a -reflection) . b = b ; :: thesis: a = b

then A1: ((a -reflection) . b) + b = 2 * b by Th3;

(a -reflection) . b = (2 * a) - b by Def4;

then ((a -reflection) . b) + b = (2 * a) - (b - b) by RLVECT_1:29

.= (2 * a) - (0. E) by RLVECT_1:15

.= 2 * a ;

hence a = b by A1, RLVECT_1:36; :: thesis: verum