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 Lm3;
then rng f c= dom (canon_image (Y,1)) ;
then A2: dom ((canon_image (Y,1)) * f) = X by A1, RELAT_1:27;
rng ((canon_image (Y,1)) * f) c= rng (canon_image (Y,1)) by RELAT_1:26;
hence (canon_image (Y,1)) * f is Function of X,(free_magma Y) by A2, FUNCT_2:2; :: thesis: verum