A1: the carrier of (Image g) = rng g by YELLOW_0:def 15;
then ( the carrier of (Image g) | g = g & the carrier of L1 = dom g ) by FUNCT_2:def 1, RELAT_1:125;
hence the carrier of (Image g) | g is Function of L1,(Image g) by A1, FUNCT_2:3; :: thesis: verum