take f = id S; :: thesis: f is isomorphic
f " = id S by TOPGRP_1:2;
hence f is isomorphic ; :: thesis: verum