theorem Th30: :: TOPGRP_1:31
for T being TopStruct
for f, g being Homeomorphism of T holds f * g is Homeomorphism of T