:: deftheorem defines Image WAYBEL18:def 6 :
for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds Image f = Y | (rng f);