theorem :: ALGSTR_4:17

for X being set holds free_magma (X,1) = X by Def13;