:: deftheorem Def9 defines free_in_itself MSAFREE4:def 9 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms MSAlgebra over S holds
( A is free_in_itself iff for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X holds
ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & f = h || G ) );