:: deftheorem Def6 defines FuncLatt UNIALG_3:def 6 :
for U01, U02 being with_const_op Universal_Algebra
for F being Function of the carrier of U01, the carrier of U02
for b₄ being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) holds
( b₄ = FuncLatt F iff for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
b₄ . U1 = GenUnivAlg H );