theorem :: ALGSTR_4:47

for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
free_magmaF f is one-to-one