theorem :: ALG_1:2

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds f * (<*> the carrier of U1) = <*> the carrier of U2 ;