let X be 1-sorted ; :: thesis: for Y being TopStruct
for f being Function of X,Y holds the carrier of (Image f) = rng f
let Y be TopStruct ; :: thesis: for f being Function of X,Y holds the carrier of (Image f) = rng f
let f be Function of X,Y; :: thesis: the carrier of (Image f) = rng f
thus the carrier of (Image f) = [#] (Y | (rng f))
.= rng f by PRE_TOPC:def 5 ; :: thesis: verum