let E be RealNormSpace; :: thesis: for a being Point of E holds (a -reflection) /" = a -reflection
let a be Point of E; :: thesis: (a -reflection) /" = a -reflection
set R = a -reflection ;
A1: rng (a -reflection) = [#] E by FUNCT_2:def 3;
A2: (a -reflection) /" = (a -reflection) " by TOPS_2:def 4;
(a -reflection) * (a -reflection) = id E by Th17;
hence (a -reflection) /" = a -reflection by A1, A2, FUNCT_2:30; :: thesis: verum