for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds the carrier of (Image f) = rng f