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