let A be 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
let G be 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
let B be Universal_Algebra; for h1, h2 being Function of A,B st h1 is_homomorphism & h2 is_homomorphism & h1 | G = h2 | G holds
h1 = h2
let h1, h2 be Function of A,B; ( h1 is_homomorphism & h2 is_homomorphism & h1 | G = h2 | G implies h1 = h2 )
assume that
A1:
h1 is_homomorphism
and
A2:
h2 is_homomorphism
and
A3:
h1 | G = h2 | G
; h1 = h2
defpred S1[ Nat] means for a being Element of A st a in G |^ $1 holds
h1 . a = h2 . a;
A4:
S1[ 0 ]
A6:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A7:
S1[
n]
;
S1[n + 1]
let a be
Element of
A;
( a in G |^ (n + 1) implies h1 . a = h2 . a )
assume that A8:
a in G |^ (n + 1)
and A9:
h1 . a <> h2 . a
;
contradiction
a nin G |^ n
by A7, A9;
then consider o being
Element of
dom the
charact of
A,
p being
Element of the
carrier of
A * such that A10:
a = (Den (o,A)) . p
and A11:
p in dom (Den (o,A))
and A12:
rng p c= G |^ n
by A8, 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:1;
then reconsider o9 =
o as
Element of
dom the
charact of
B by FINSEQ_3:29;
A13:
Operations A = rng the
charact of
A
;
A14:
Operations B = rng the
charact of
B
;
then A15:
h1 . a = (Den (o9,B)) . (h1 * p)
by A1, A10, A11, A13, ALG_1:def 1;
A16:
h2 . a = (Den (o9,B)) . (h2 * p)
by A2, A10, A11, A13, A14, ALG_1:def 1;
hence
contradiction
by A9, A12, A15, A16, Th1;
verum
end;
A18:
for n being Nat holds S1[n]
from NAT_1:sch 2(A4, A6);
hence
h1 = h2
by FUNCT_2:63; verum