for T being TopStruct
for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"