theorem :: TOPGRP_1:32

for T being TopStruct
for f, g being Homeomorphism of T
for a, b being Element of (HomeoGroup T) st f = a & g = b holds
a * b = g * f by Def5;