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 & p1 = p2 )
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 & p1 = p2 )
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 & p1 = p2 ) )
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 & p1 = p2 )
thus A3:
o1 = o2
by A1, A2, Lm2; :: thesis: p1 = p2
reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:9;
set G' = G \/ {the carrier of A};
reconsider G' = G \/ {the carrier of A} as non empty set ;
deffunc H1( set ) -> set = root-tree [0 ,$1];
consider g being Function such that
A4:
( dom g = G & ( for x being set st x in G holds
g . x = H1(x) ) )
from FUNCT_1:sch 3();
set X = [:{0 },G':];
set B = FreeUnivAlgNSG S,[:{0 },G':];
A5:
signature (FreeUnivAlgNSG S,[:{0 },G':]) = S
by FREEALG:4;
A6:
Terminals (DTConUA S,[:{0 },G':]) = [:{0 },G':]
by FREEALG:3;
rng g c= FreeGenSetNSG S,[:{0 },G':]
proof
let b be
set ;
:: according to TARSKI:def 3 :: thesis: ( b nin rng g or not b nin FreeGenSetNSG S,[:{0 },G':] )
assume
b in rng g
;
:: thesis: not b nin FreeGenSetNSG S,[:{0 },G':]
then consider a being
set such that A7:
(
a in dom g &
b = g . a )
by FUNCT_1:def 5;
reconsider a =
a as
Element of
A by A4, A7;
(
a in G' &
0 in {0 } )
by A4, A7, TARSKI:def 1, XBOOLE_0:def 3;
then A8:
[0 ,a] in [:{0 },G':]
by ZFMISC_1:106;
then reconsider s =
[0 ,a] as
Symbol of
(DTConUA S,[:{0 },G':]) by A6;
root-tree s in FreeGenSetNSG S,
[:{0 },G':]
by A6, A8;
hence
not
b nin FreeGenSetNSG S,
[:{0 },G':]
by A4, A7;
:: thesis: verum
end;
then reconsider g = g as Function of G,the carrier of (FreeUnivAlgNSG S,[:{0 },G':]) by A4, FUNCT_2:4, XBOOLE_1:1;
signature (FreeUnivAlgNSG S,[:{0 },G':]) = S
by FREEALG:4;
then
A, FreeUnivAlgNSG S,[:{0 },G':] are_similar
by UNIALG_2:def 2;
then consider h being Function of A,(FreeUnivAlgNSG S,[:{0 },G':]) such that
A9:
( h is_homomorphism A, FreeUnivAlgNSG S,[:{0 },G':] & h | G = g )
by FREEALG:def 6;
defpred S1[ Nat] means for a1, a2 being set st a1 in G |^ $1 & a2 in G |^ $1 & h . a1 = h . a2 holds
a1 = a2;
A10:
G |^ 0 = G
by Th18;
A11:
( len S = len the charact of (FreeUnivAlgNSG S,[:{0 },G':]) & len S = len the charact of A )
by A5, UNIALG_1:def 11;
then A12:
( dom S = dom the charact of (FreeUnivAlgNSG S,[:{0 },G':]) & dom S = dom the charact of A )
by FINSEQ_3:31;
A13:
now let o be
Element of
dom the
charact of
A;
:: thesis: for p being FinSequence of A st p in dom (Den o,A) holds
( len p = S . o & len (h * p) = S . o & h . ((Den o,A) . p) = o -tree (h * p) )let p be
FinSequence of
A;
:: thesis: ( p in dom (Den o,A) implies ( len p = S . o & len (h * p) = S . o & h . ((Den o,A) . p) = o -tree (h * p) ) )assume A14:
p in dom (Den o,A)
;
:: thesis: ( len p = S . o & len (h * p) = S . o & h . ((Den o,A) . p) = o -tree (h * p) )reconsider q =
p as
FinSequence of
A ;
reconsider hq =
h * q as
FinSequence of
(FreeUnivAlgNSG S,[:{0 },G':]) ;
reconsider op =
Den o,
A as
Element of
Operations A ;
reconsider on =
o as
Element of
NAT ;
reconsider o' =
on as
OperSymbol of
(FreeUnivAlgNSG S,[:{0 },G':]) by A11, FINSEQ_3:31;
reconsider op' =
Den o',
(FreeUnivAlgNSG S,[:{0 },G':]) as
Element of
Operations (FreeUnivAlgNSG S,[:{0 },G':]) ;
reconsider j =
S . o' as
Element of
NAT ;
dom op = (arity op) -tuples_on the
carrier of
A
by UNIALG_2:2;
then A15:
len p =
arity op
by A14, FINSEQ_1:def 18
.=
j
by A12, UNIALG_1:def 11
;
hence
(
len p = S . o &
len (h * p) = S . o )
by FINSEQ_2:37;
:: thesis: h . ((Den o,A) . p) = o -tree (h * p)A16:
h . (op . q) = op' . hq
by A14, A9, ALG_1:def 1;
A17:
In o',
(dom the charact of (FreeUnivAlgNSG S,[:{0 },G':])) = o'
by FUNCT_7:def 1;
(
o' in dom S &
len hq = S . o' )
by A12, A15, FINSEQ_2:37;
hence
h . ((Den o,A) . p) = o -tree (h * p)
by A17, A16, Th17;
:: thesis: verum end;
A18:
S1[ 0 ]
A20:
now let o be
Element of
dom the
charact of
A;
:: thesis: for p being Element of the carrier of A * st p in dom (Den o,A) holds
for x being set st x in G holds
not h . ((Den o,A) . p) = h . xlet p be
Element of the
carrier of
A * ;
:: thesis: ( p in dom (Den o,A) implies for x being set st x in G holds
not h . ((Den o,A) . p) = h . x )assume
p in dom (Den o,A)
;
:: thesis: for x being set st x in G holds
not h . ((Den o,A) . p) = h . xthen A21:
h . ((Den o,A) . p) = o -tree (h * p)
by A13;
let x be
set ;
:: thesis: ( x in G implies not h . ((Den o,A) . p) = h . x )assume A22:
x in G
;
:: thesis: not h . ((Den o,A) . p) = h . xthen A23:
h . x =
g . x
by A9, FUNCT_1:72
.=
H1(
x)
by A22, A4
;
assume
h . ((Den o,A) . p) = h . x
;
:: thesis: contradictionhence
contradiction
by A23, A21, TREES_4:17;
:: thesis: verum end;
A24:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A25:
S1[
k]
;
:: thesis: S1[k + 1]
defpred S2[
set ]
means ex
o being
Element of
dom the
charact of
A ex
p being
Element of the
carrier of
A * st
( $1
= (Den o,A) . p &
p in dom (Den o,A) &
rng p c= G |^ k );
let a1,
a2 be
set ;
:: thesis: ( a1 in G |^ (k + 1) & a2 in G |^ (k + 1) & h . a1 = h . a2 implies a1 = a2 )
assume A26:
(
a1 in G |^ (k + 1) &
a2 in G |^ (k + 1) &
h . a1 = h . a2 )
;
:: thesis: a1 = a2
per cases
( ( a1 in G & a2 in G ) or ( S2[a1] & S2[a2] ) or ( a1 in G & S2[a2] ) or ( S2[a1] & a2 in G ) )
by A26, Th23;
suppose A28:
(
S2[
a1] &
S2[
a2] )
;
:: thesis: a1 = a2then consider b1 being
Element of
dom the
charact of
A,
q1 being
Element of the
carrier of
A * such that A29:
(
a1 = (Den b1,A) . q1 &
q1 in dom (Den b1,A) &
rng q1 c= G |^ k )
;
consider b2 being
Element of
dom the
charact of
A,
q2 being
Element of the
carrier of
A * such that A30:
(
a2 = (Den b2,A) . q2 &
q2 in dom (Den b2,A) &
rng q2 c= G |^ k )
by A28;
b1 -tree (h * q1) =
h . a1
by A13, A29
.=
b2 -tree (h * q2)
by A13, A30, A26
;
then A31:
(
b1 = b2 &
h * q1 = h * q2 )
by TREES_4:15;
(
len q1 = S . b1 &
len q2 = S . b2 )
by A29, A30, A13;
then A32:
(
dom q1 = Seg (len q1) &
dom q2 = Seg (len q1) )
by A31, FINSEQ_1:def 3;
hence
a1 = a2
by A29, A30, A31, A32, FINSEQ_1:17;
:: thesis: verum end;
end;
A34:
for k being Nat holds S1[k]
from NAT_1:sch 2(A18, A24);
reconsider q1 = p1, q2 = p2 as FinSequence of A by A1, FINSEQ_1:def 11;
o1 -tree (h * q1) =
h . ((Den o1,A) . p1)
by A1, A13
.=
o2 -tree (h * q2)
by A2, A1, A13
;
then A35:
h * p1 = h * p2
by TREES_4:15;
( len q1 = S . o1 & len q2 = S . o2 )
by A1, A13;
then A36:
( dom q1 = Seg (len q1) & dom q2 = Seg (len q1) )
by A3, FINSEQ_1:def 3;
hence
p1 = p2
by A36, FINSEQ_1:17; :: thesis: verum