let A be partial non-empty UAStr ; for P being a_partition of A holds A can_be_characterized_by MSSign (A,P)
let P be a_partition of A; A can_be_characterized_by MSSign (A,P)
set S = MSSign (A,P);
P = the carrier of (MSSign (A,P))
by Def14;
then reconsider Z = id P as ManySortedSet of the carrier of (MSSign (A,P)) ;
deffunc H1( OperSymbol of (MSSign (A,P))) -> Element of bool [:( the carrier of A *), the carrier of A:] = (Den (($1 `1),A)) | (product ($1 `2));
consider D being ManySortedSet of the carrier' of (MSSign (A,P)) such that
A1:
for o being OperSymbol of (MSSign (A,P)) holds D . o = H1(o)
from PBOOLE:sch 5();
deffunc H2( OperSymbol of A) -> set = { a where a is OperSymbol of (MSSign (A,P)) : a `1 = $1 } ;
consider Q being ManySortedSet of dom the charact of A such that
A2:
for o being OperSymbol of A holds Q . o = H2(o)
from PBOOLE:sch 5();
A3:
dom Q = dom the charact of A
by PARTFUN1:def 2;
A4:
the carrier of (MSSign (A,P)) = P
by Def14;
A5:
the carrier' of (MSSign (A,P)) = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) }
by Def14;
Q is non-empty
proof
let x be
object ;
FUNCT_1:def 9 ( not x in proj1 Q or not Q . x is empty )
assume
x in dom Q
;
not Q . x is empty
then reconsider o =
x as
OperSymbol of
A ;
set y = the
Element of
dom (Den (o,A));
reconsider y = the
Element of
dom (Den (o,A)) as
Element of the
carrier of
A * ;
A6:
rng y c= the
carrier of
A
;
the
carrier of
A = union P
by EQREL_1:def 4;
then consider f being
Function such that A7:
dom f = dom y
and A8:
rng f c= P
and A9:
y in product f
by A6, Th5;
dom y = Seg (len y)
by FINSEQ_1:def 3;
then
f is
FinSequence
by A7, FINSEQ_1:def 2;
then
f is
FinSequence of
P
by A8, FINSEQ_1:def 4;
then reconsider f =
f as
Element of
P * by FINSEQ_1:def 11;
product f meets dom (Den (o,A))
by A9, XBOOLE_0:3;
then A10:
[o,f] in the
carrier' of
(MSSign (A,P))
by A5;
A11:
[o,f] `1 = o
;
Q . o = { a where a is OperSymbol of (MSSign (A,P)) : a `1 = o }
by A2;
then
[o,f] in Q . x
by A10, A11;
hence
not
Q . x is
empty
;
verum
end;
then reconsider Q = Q as non-empty Function ;
D is ManySortedFunction of (Z #) * the Arity of (MSSign (A,P)),Z * the ResultSort of (MSSign (A,P))
proof
let x be
object ;
PBOOLE:def 15 ( not x in the carrier' of (MSSign (A,P)) or D . x is Element of bool [:(((Z #) * the Arity of (MSSign (A,P))) . x),((Z * the ResultSort of (MSSign (A,P))) . x):] )
assume A12:
x in the
carrier' of
(MSSign (A,P))
;
D . x is Element of bool [:(((Z #) * the Arity of (MSSign (A,P))) . x),((Z * the ResultSort of (MSSign (A,P))) . x):]
then consider o being
OperSymbol of
A,
p being
Element of
P * such that A13:
x = [o,p]
and A14:
product p meets dom (Den (o,A))
by A5;
reconsider xx =
x as
OperSymbol of
(MSSign (A,P)) by A12;
A15:
rng the
ResultSort of
(MSSign (A,P)) c= the
carrier of
(MSSign (A,P))
;
A16:
dom the
Arity of
(MSSign (A,P)) = the
carrier' of
(MSSign (A,P))
by FUNCT_2:def 1;
A17:
rng p c= P
;
A18:
the
Arity of
(MSSign (A,P)) . x = p
by A13, A14, Def14;
A19:
(Z #) . p = product (Z * p)
by A4, FINSEQ_2:def 5;
Z * p = p
by A17, RELAT_1:53;
then A20:
((Z #) * the Arity of (MSSign (A,P))) . x = product p
by A12, A16, A18, A19, FUNCT_1:13;
A21:
(Den (o,A)) .: (product p) c= the
ResultSort of
(MSSign (A,P)) . x
by A13, A14, Def14;
A22:
xx `2 = p
by A13;
A23:
xx `1 = o
by A13;
A24:
rng ((Den (o,A)) | (product p)) = (Den (o,A)) .: (product p)
by RELAT_1:115;
A25:
D . xx = (Den (o,A)) | (product p)
by A1, A22, A23;
Den (
o,
A)
is_exactly_partitable_wrt P
by Def10;
then A26:
product p c= dom (Den (o,A))
by A14;
A27:
Z * the
ResultSort of
(MSSign (A,P)) = the
ResultSort of
(MSSign (A,P))
by A4, A15, RELAT_1:53;
dom ((Den (o,A)) | (product p)) = product p
by A26, RELAT_1:62;
hence
D . x is
Element of
bool [:(((Z #) * the Arity of (MSSign (A,P))) . x),((Z * the ResultSort of (MSSign (A,P))) . x):]
by A20, A21, A24, A25, A27, FUNCT_2:2;
verum
end;
then reconsider D = D as ManySortedFunction of (Z #) * the Arity of (MSSign (A,P)),Z * the ResultSort of (MSSign (A,P)) ;
A28:
Union Q = the carrier' of (MSSign (A,P))
then reconsider Q = Q as IndexedPartition of the carrier' of (MSSign (A,P)) by A28, Th13;
take G = MSAlgebra(# Z,D #); PUA2MSS1:def 16 ex P being IndexedPartition of the carrier' of (MSSign (A,P)) st A can_be_characterized_by MSSign (A,P),G,P
take
Q
; A can_be_characterized_by MSSign (A,P),G,Q
rng (id P) is a_partition of A
;
hence
the Sorts of G is IndexedPartition of A
by Def11; PUA2MSS1:def 15 ( dom Q = dom the charact of A & ( for o being OperSymbol of A holds the Charact of G | (Q . o) is IndexedPartition of Den (o,A) ) )
thus
dom Q = dom the charact of A
by PARTFUN1:def 2; for o being OperSymbol of A holds the Charact of G | (Q . o) is IndexedPartition of Den (o,A)
let o be OperSymbol of A; the Charact of G | (Q . o) is IndexedPartition of Den (o,A)
reconsider PP = { (product p) where p is Element of P * : verum } as a_partition of the carrier of A * by Th8;
reconsider QQ = { (a /\ (dom (Den (o,A)))) where a is Element of PP : a meets dom (Den (o,A)) } as a_partition of dom (Den (o,A)) by Th10;
set F = the Charact of G | (Q . o);
A39:
Q . o in rng Q
by A3, FUNCT_1:def 3;
A40:
dom D = the carrier' of (MSSign (A,P))
by PARTFUN1:def 2;
then A41:
dom ( the Charact of G | (Q . o)) = Q . o
by A39, RELAT_1:62;
reconsider F = the Charact of G | (Q . o) as non empty Function by A39, A40;
reconsider Qo = Q . o as non empty set ;
reconsider RR = { ((Den (o,A)) | a) where a is Element of QQ : verum } as a_partition of Den (o,A) by Th11;
A42:
Q . o = { a where a is OperSymbol of (MSSign (A,P)) : a `1 = o }
by A2;
rng F c= RR
proof
let y be
object ;
TARSKI:def 3 ( not y in rng F or y in RR )
assume
y in rng F
;
y in RR
then consider x being
object such that A43:
x in dom F
and A44:
y = F . x
by FUNCT_1:def 3;
x in (dom the Charact of G) /\ (Q . o)
by A43, RELAT_1:61;
then
x in Q . o
by XBOOLE_0:def 4;
then consider a being
OperSymbol of
(MSSign (A,P)) such that A45:
x = a
and A46:
a `1 = o
by A42;
a in the
carrier' of
(MSSign (A,P))
;
then consider s being
OperSymbol of
A,
p being
Element of
P * such that A47:
a = [s,p]
and A48:
product p meets dom (Den (s,A))
by A5;
A49:
s = o
by A46, A47;
A50:
a `2 = p
by A47;
A51:
product p in PP
;
A52:
Den (
o,
A)
is_exactly_partitable_wrt P
by Def10;
A53:
(product p) /\ (dom (Den (o,A))) in QQ
by A48, A49, A51;
product p c= dom (Den (o,A))
by A48, A49, A52;
then
product p in QQ
by A53, XBOOLE_1:28;
then A54:
(Den (o,A)) | (product p) in RR
;
y = D . a
by A43, A44, A45, FUNCT_1:47;
hence
y in RR
by A1, A46, A50, A54;
verum
end;
then reconsider F = F as Function of Qo,RR by A41, FUNCT_2:2;
A55:
RR c= rng F
proof
let x be
object ;
TARSKI:def 3 ( not x in RR or x in rng F )
assume
x in RR
;
x in rng F
then consider a being
Element of
QQ such that A56:
x = (Den (o,A)) | a
;
a in QQ
;
then consider b being
Element of
PP such that A57:
a = b /\ (dom (Den (o,A)))
and A58:
b meets dom (Den (o,A))
;
b in PP
;
then consider p being
Element of
P * such that A59:
b = product p
;
Den (
o,
A)
is_exactly_partitable_wrt P
by Def10;
then
product p c= dom (Den (o,A))
by A58, A59;
then A60:
b = a
by A57, A59, XBOOLE_1:28;
A61:
[o,p] in the
carrier' of
(MSSign (A,P))
by A5, A58, A59;
A62:
[o,p] `1 = o
;
A63:
[o,p] `2 = p
;
A64:
[o,p] in dom D
by A61, PARTFUN1:def 2;
A65:
[o,p] in Q . o
by A42, A61, A62;
D . [o,p] = x
by A1, A56, A59, A60, A61, A62, A63;
hence
x in rng F
by A64, A65, FUNCT_1:50;
verum
end;
F is one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in proj1 F or not x2 in proj1 F or not F . x1 = F . x2 or x1 = x2 )
assume that A66:
x1 in dom F
and A67:
x2 in dom F
and A68:
F . x1 = F . x2
;
x1 = x2
consider a1 being
OperSymbol of
(MSSign (A,P)) such that A69:
x1 = a1
and A70:
a1 `1 = o
by A41, A42, A66;
consider a2 being
OperSymbol of
(MSSign (A,P)) such that A71:
x2 = a2
and A72:
a2 `1 = o
by A41, A42, A67;
a1 in the
carrier' of
(MSSign (A,P))
;
then consider o1 being
OperSymbol of
A,
p1 being
Element of
P * such that A73:
a1 = [o1,p1]
and A74:
product p1 meets dom (Den (o1,A))
by A5;
a2 in the
carrier' of
(MSSign (A,P))
;
then consider o2 being
OperSymbol of
A,
p2 being
Element of
P * such that A75:
a2 = [o2,p2]
and A76:
product p2 meets dom (Den (o2,A))
by A5;
A77:
F . x1 = D . a1
by A66, A69, FUNCT_1:47;
A78:
F . x1 = D . a2
by A67, A68, A71, FUNCT_1:47;
A79:
a1 `2 = p1
by A73;
A80:
a2 `2 = p2
by A75;
A81:
F . x1 = (Den (o,A)) | (product p1)
by A1, A70, A77, A79;
A82:
F . x1 = (Den (o,A)) | (product p2)
by A1, A72, A78, A80;
A83:
Den (
o,
A)
is_exactly_partitable_wrt P
by Def10;
A84:
o = o1
by A70, A73;
A85:
o = o2
by A72, A75;
A86:
product p1 c= dom (Den (o,A))
by A74, A83, A84;
A87:
product p2 c= dom (Den (o,A))
by A76, A83, A85;
product p1 = dom ((Den (o,A)) | (product p1))
by A86, RELAT_1:62;
hence
x1 = x2
by A69, A71, A73, A75, A81, A82, A84, A85, A87, Th2, RELAT_1:62;
verum
end;
hence
the Charact of G | (Q . o) is IndexedPartition of Den (o,A)
by A55, Th14; verum