:: deftheorem Def10 defines Univ_Alg-yielding PRALG_1:def 10 :
for IT being Function holds
( IT is Univ_Alg-yielding iff for x being object st x in dom IT holds
IT . x is Universal_Algebra );