let s be Real; :: thesis: for p being Point of (TOP-REAL 2) st (Rotate s) . p = 0. (TOP-REAL 2) holds
p = 0. (TOP-REAL 2)
let p be Point of (TOP-REAL 2); :: thesis: ( (Rotate s) . p = 0. (TOP-REAL 2) implies p = 0. (TOP-REAL 2) )
|.p.| = |.((Rotate s) . p).| by Th41;
hence ( (Rotate s) . p = 0. (TOP-REAL 2) implies p = 0. (TOP-REAL 2) ) by TOPRNS_1:23, TOPRNS_1:24; :: thesis: verum