for X being TopStruct
for Y, Z being non empty TopStruct
for f being Function of X,Y
for g being Function of X,Z holds
( dom f = dom g & dom f = the carrier of X & dom f = [#] X )