theorem :: AOFA_000:35
for A being free Universal_Algebra
for G being GeneratorSet of A
for B being Universal_Algebra
for h1, h2 being Function of A,B st h1 is_homomorphism & h2 is_homomorphism & h1 | G = h2 | G holds
h1 = h2