let s be Real; :: thesis: (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2)
let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def 8 :: thesis: ((Rotate s) * (Rotate (- s))) . p = (id (TOP-REAL 2)) . p
set f = Rotate s;
set g = Rotate (- s);
thus ((Rotate s) * (Rotate (- s))) . p = (Rotate s) . ((Rotate (- s)) . p) by FUNCT_2:15
.= p by Th46
.= (id (TOP-REAL 2)) . p ; :: thesis: verum