A1: rng (id (Image g)) = the carrier of (Image g)
.= rng g by YELLOW_0:def 15 ;
dom (id (Image g)) = the carrier of (Image g) ;
hence id (Image g) is Function of (Image g),L2 by A1, RELSET_1:4; :: thesis: verum