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