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