let A be free Universal_Algebra; :: thesis: for o1, o2 being OperSymbol of A
for p1, p2 being FinSequence st p1 in dom (Den o1,A) & p2 in dom (Den o2,A) & (Den o1,A) . p1 = (Den o2,A) . p2 holds
o1 = o2
consider G being free GeneratorSet of A;
let o1, o2 be OperSymbol of A; :: thesis: for p1, p2 being FinSequence st p1 in dom (Den o1,A) & p2 in dom (Den o2,A) & (Den o1,A) . p1 = (Den o2,A) . p2 holds
o1 = o2
let p1, p2 be FinSequence; :: thesis: ( p1 in dom (Den o1,A) & p2 in dom (Den o2,A) & (Den o1,A) . p1 = (Den o2,A) . p2 implies o1 = o2 )
assume that
A1: ( p1 in dom (Den o1,A) & p2 in dom (Den o2,A) ) and
A2: (Den o1,A) . p1 = (Den o2,A) . p2 ; :: thesis: o1 = o2
reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:9;
consider B being Universal_Algebra such that
A3: ( the carrier of B = NAT & signature B = S ) and
A4: for i, j being Nat st i in dom S & j = S . i holds
the charact of B . i = (j -tuples_on NAT ) --> i by Th14;
reconsider f = G --> 0 as Function of G,the carrier of B by A3;
A,B are_similar by A3, UNIALG_2:def 2;
then consider h being Function of A,B such that
A5: ( h is_homomorphism A,B & h | G = f ) by FREEALG:def 6;
A6: ( len S = len the charact of B & len S = len the charact of A ) by A3, UNIALG_1:def 11;
then A7: ( dom S = dom the charact of B & dom S = dom the charact of A ) by FINSEQ_3:31;
reconsider b1 = o1, b2 = o2 as OperSymbol of B by A6, FINSEQ_3:31;
reconsider n1 = o1, n2 = o2 as Element of NAT ;
reconsider j1 = S . n1, j2 = S . n2 as Element of NAT ;
reconsider x1 = p1, x2 = p2 as FinSequence of A by A1, FINSEQ_1:def 11;
reconsider h1 = h * x1, h2 = h * x2 as FinSequence of NAT by A3;
reconsider oo1 = Den o1,A, oo2 = Den o2,A as Element of Operations A ;
A8: ( dom oo1 = (arity oo1) -tuples_on the carrier of A & dom oo2 = (arity oo2) -tuples_on the carrier of A ) by UNIALG_2:2;
then len x1 = arity oo1 by A1, FINSEQ_1:def 18
.= j1 by A7, UNIALG_1:def 11 ;
then len h1 = j1 by FINSEQ_2:37;
then A9: h1 is Element of j1 -tuples_on NAT by FINSEQ_2:110;
len x2 = arity oo2 by A8, A1, FINSEQ_1:def 18
.= j2 by A7, UNIALG_1:def 11 ;
then len h2 = j2 by FINSEQ_2:37;
then A10: h2 is Element of j2 -tuples_on NAT by FINSEQ_2:110;
( Den o1,A = the charact of A . n1 & Den o1,A is Element of Operations A & Den b1,B = the charact of B . n1 & Den b1,B is Element of Operations B & Den o2,A = the charact of A . n2 & Den o2,A is Element of Operations A & Den b2,B = the charact of B . n2 & Den b2,B is Element of Operations B ) ;
then A11: ( h . ((Den o1,A) . x1) = (Den b1,B) . h1 & h . ((Den o2,A) . x2) = (Den b2,B) . h2 ) by A1, A5, ALG_1:def 1;
( Den b1,B = (j1 -tuples_on NAT ) --> n1 & Den b2,B = (j2 -tuples_on NAT ) --> n2 ) by A4, A7;
then ( (Den b1,B) . h1 = n1 & (Den b2,B) . h2 = n2 ) by A9, A10, FUNCOP_1:13;
hence o1 = o2 by A2, A11; :: thesis: verum