let A be free Universal_Algebra; :: thesis: for G being GeneratorSet of A
for B being Universal_Algebra
for h1, h2 being Function of A,B st h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1 | G = h2 | G holds
h1 = h2
let G be GeneratorSet of A; :: thesis: for B being Universal_Algebra
for h1, h2 being Function of A,B st h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1 | G = h2 | G holds
h1 = h2
let B be Universal_Algebra; :: thesis: for h1, h2 being Function of A,B st h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1 | G = h2 | G holds
h1 = h2
let h1, h2 be Function of A,B; :: thesis: ( h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1 | G = h2 | G implies h1 = h2 )
assume A1: ( h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1 | G = h2 | G ) ; :: thesis: h1 = h2
defpred S₁[ Nat] means for a being Element of A st a in G |^ $1 holds
h1 . a = h2 . a;
A2: S₁[ 0 ]

proof

let a be Element of A; :: thesis: ( a in G |^ 0 implies h1 . a = h2 . a )
assume a in G |^ 0 ; :: thesis: h1 . a = h2 . a
then a in G by Th18;
then ( h1 . a = (h1 | G) . a & h2 . a = (h2 | G) . a ) by FUNCT_1:72;
hence h1 . a = h2 . a by A1; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let a be Element of A; :: thesis: ( a in G |^ (n + 1) implies h1 . a = h2 . a )
assume A5: ( a in G |^ (n + 1) & h1 . a <> h2 . a ) ; :: thesis: contradiction
then a nin G |^ n by A4;
then consider o being Element of dom the charact of A, p being Element of the carrier of A * such that
A6: ( a = (Den o,A) . p & p in dom (Den o,A) & rng p c= G |^ n ) by A5, Th20;
A,B are_similar by A1, ALG_1:def 1;
then len the charact of A = len the charact of B by UNIALG_2:3;
then reconsider o' = o as Element of dom the charact of B by FINSEQ_3:31;
( Operations A = rng the charact of A & Operations B = rng the charact of B ) ;
then A7: ( h1 . a = (Den o',B) . (h1 * p) & h2 . a = (Den o',B) . (h2 * p) ) by A6, A1, ALG_1:def 1;

now

( dom h1 = the carrier of A & dom h2 = the carrier of A ) by FUNCT_2:def 1;
hence ( G |^ n c= dom h1 & G |^ n c= dom h2 ) ; :: thesis: for x being set st x in G |^ n holds
h1 . x = h2 . x
let x be set ; :: thesis: ( x in G |^ n implies h1 . x = h2 . x )
assume x in G |^ n ; :: thesis: h1 . x = h2 . x
hence h1 . x = h2 . x by A4; :: thesis: verum

end;

hence contradiction by A5, A7, A6, Th1; :: thesis: verum

end;

A8: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);

now

let a be Element of A; :: thesis: h1 . a = h2 . a
ex n being Nat st a in G |^ n by Th30;
hence h1 . a = h2 . a by A8; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:113; :: thesis: verum