let X, Y be non empty set ; :: thesis: for f being Function of X,Y holds (canon_image (Y,1)) * f is Function of X,(free_magma Y)
let f be Function of X,Y; :: thesis: (canon_image (Y,1)) * f is Function of X,(free_magma Y)
A1: dom f = X by FUNCT_2:def 1;
dom (canon_image (Y,1)) = Y by Lm2;
then rng f c= dom (canon_image (Y,1)) ;
then A2: dom ((canon_image (Y,1)) * f) = X by A1, RELAT_1:46;
rng ((canon_image (Y,1)) * f) c= rng (canon_image (Y,1)) by RELAT_1:45;
hence (canon_image (Y,1)) * f is Function of X,(free_magma Y) by A2, FUNCT_2:4; :: thesis: verum