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;
thus the carrier of (Image g) |` g is Function of L1,(Image g) by A2, A1, FUNCT_2:1; :: thesis: verum