theorem Th46: :: ALGSTR_4:46

for X, Y being non empty set
for f being Function of X,Y holds free_magmaF (id X) = id (dom (free_magmaF f))