for X, Y, Z being non empty set
for f being Function of X,Y
for g being Function of X,Z st Y c= Z & f = g holds
free_magmaF f = free_magmaF g