let E be RealNormSpace; :: thesis: for a being Point of E holds (a -reflection) * (a -reflection) = id E
let a be Point of E; :: thesis: (a -reflection) * (a -reflection) = id E
set R = a -reflection ;
let b be Point of E; :: according to FUNCT_2:def 8 :: thesis: ((a -reflection) * (a -reflection)) . b = (id E) . b
thus ((a -reflection) * (a -reflection)) . b = (a -reflection) . ((a -reflection) . b) by FUNCT_2:15
.= (2 * a) - ((a -reflection) . b) by Def4
.= (2 * a) - ((2 * a) - b) by Def4
.= ((2 * a) - (2 * a)) + b by RLVECT_1:29
.= (0. E) + b by RLVECT_1:5
.= b
.= (id E) . b ; :: thesis: verum