:: deftheorem defines free FREEALG:def 5 :
for U0 being Universal_Algebra
for IT being GeneratorSet of U0 holds
( IT is free iff for U1 being Universal_Algebra st U0,U1 are_similar holds
for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st
( h is_homomorphism & h | IT = f ) );