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