let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is one-to-one holds
free_magmaF f is one-to-one
let f be Function of X,Y; :: thesis: ( f is one-to-one implies free_magmaF f is one-to-one )
assume A1: f is one-to-one ; :: thesis: free_magmaF f is one-to-one
then A2: (f ") * f = id (dom f) by FUNCT_1:39;
set Y9 = rng f;
dom f = X by FUNCT_2:def 1;
then reconsider f1 = f as Function of X,(rng f) by FUNCT_2:1;
reconsider f2 = f1 " as Function of (rng f),X by A1, FUNCT_2:25;
f2 * f1 = id X by A2, FUNCT_2:def 1;
then (free_magmaF f2) * (free_magmaF f1) = free_magmaF (id X) by Th44;
then (free_magmaF f2) * (free_magmaF f) = free_magmaF (id X) by Th45;
then (free_magmaF f2) * (free_magmaF f) = id (dom (free_magmaF f)) by Th46;
hence free_magmaF f is one-to-one by FUNCT_1:31; :: thesis: verum