let T be TopStruct ; :: thesis: for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
let f, g be Homeomorphism of T; :: thesis: f * g is Homeomorphism of T
( not T is empty or T is empty ) ;
hence f * g is being_homeomorphism by TOPS_2:57; :: according to TOPGRP_1:def 4 :: thesis: verum