let s be Real; :: thesis: for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p
let p be Point of (TOP-REAL 2); :: thesis: (Rotate s) . ((Rotate (- s)) . p) = p
set f = Rotate s;
set g = Rotate (- s);

per cases ( p <> 0. (TOP-REAL 2) or p = 0. (TOP-REAL 2) ) ;

suppose A1: p <> 0. (TOP-REAL 2) ; :: thesis: (Rotate s) . ((Rotate (- s)) . p) = p

then consider i being Integer such that
A2: Arg ((Rotate (- s)) . p) = ((- s) + (Arg p)) + ((2 * PI) * i) by Th43;
consider j being Integer such that
A3: Arg ((Rotate s) . ((Rotate (- s)) . p)) = (s + (Arg ((Rotate (- s)) . p))) + ((2 * PI) * j) by A1, Th45, Th43;
A4: |.((Rotate s) . ((Rotate (- s)) . p)).| = |.((Rotate (- s)) . p).| by Th41
.= |.p.| by Th41 ;
Arg ((Rotate s) . ((Rotate (- s)) . p)) = (Arg p) + ((2 * PI) * (i + j)) by A2, A3;
hence (Rotate s) . ((Rotate (- s)) . p) = p by A4, Th35; :: thesis: verum

end;

suppose A5: p = 0. (TOP-REAL 2) ; :: thesis: (Rotate s) . ((Rotate (- s)) . p) = p

(Rotate s) . ((Rotate (- s)) . (0. (TOP-REAL 2))) = (Rotate s) . (0. (TOP-REAL 2)) by Th44
.= 0. (TOP-REAL 2) by Th44 ;
hence (Rotate s) . ((Rotate (- s)) . p) = p by A5; :: thesis: verum

end;

end;