:: deftheorem defines is_homomorphism ALG_1:def 1 :
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_homomorphism iff ( U1,U2 are_similar & ( for n being Nat st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = the charact of U1 . n & o2 = the charact of U2 . n holds
for x being FinSequence of U1 st x in dom o1 holds
f . (o1 . x) = o2 . (f * x) ) ) );