theorem :: ALGSTR_4:48

for X, Y being non empty set
for f being Function of X,Y st f is onto holds
free_magmaF f is onto