let A be partial non-empty UAStr ; for P being a_partition of A st P = Class (LimDomRel A) holds
for S being non empty non void ManySortedSign st A can_be_characterized_by S holds
MSSign (A,P) is_rougher_than S
let P be a_partition of A; ( P = Class (LimDomRel A) implies for S being non empty non void ManySortedSign st A can_be_characterized_by S holds
MSSign (A,P) is_rougher_than S )
assume A1:
P = Class (LimDomRel A)
; for S being non empty non void ManySortedSign st A can_be_characterized_by S holds
MSSign (A,P) is_rougher_than S
set S1 = MSSign (A,P);
let S2 be non empty non void ManySortedSign ; ( A can_be_characterized_by S2 implies MSSign (A,P) is_rougher_than S2 )
given G being MSAlgebra over S2, Q being IndexedPartition of the carrier' of S2 such that A2:
A can_be_characterized_by S2,G,Q
; PUA2MSS1:def 16 MSSign (A,P) is_rougher_than S2
A3:
the Sorts of G is IndexedPartition of A
by A2;
A4:
dom Q = dom the charact of A
by A2;
reconsider G = G as non-empty MSAlgebra over S2 by A3, MSUALG_1:def 3;
reconsider R = the Sorts of G as IndexedPartition of A by A2;
A5:
dom R = the carrier of S2
by PARTFUN1:def 2;
then reconsider SG = the Sorts of G as Function of the carrier of S2,(rng R) by RELSET_1:4;
A6:
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;
A7:
the carrier of (MSSign (A,P)) = P
by Def14;
defpred S1[ object , object ] means ex D1, D2 being set st
( D1 = $1 & D2 = $2 & D1 c= D2 );
A8:
rng R is_finer_than P
by A1, Th26;
A9:
for r being object st r in rng R holds
ex p being object st
( p in P & S1[r,p] )
consider em being Function such that
A11:
( dom em = rng R & rng em c= P )
and
A12:
for r being object st r in rng R holds
S1[r,em . r]
from FUNCT_1:sch 6(A9);
reconsider em = em as Function of (rng R),P by A11, FUNCT_2:2;
A13:
for a being set st a in rng R holds
a c= em . a
A14:
dom (em * R) = dom R
by A11, RELAT_1:27;
rng (em * R) = rng em
by A11, RELAT_1:28;
then reconsider f = em * R as Function of the carrier of S2, the carrier of (MSSign (A,P)) by A5, A7, A14, FUNCT_2:2;
take
f
; PUA2MSS1:def 13 ex g being Function st
( f,g form_morphism_between S2, MSSign (A,P) & rng f = the carrier of (MSSign (A,P)) & rng g = the carrier' of (MSSign (A,P)) )
defpred S2[ object , object ] means ex p being FinSequence of P ex o being OperSymbol of S2 st
( $2 = [(Q -index_of $1),p] & $1 = o & Args (o,G) c= product p );
A15:
for s2 being object st s2 in the carrier' of S2 holds
ex s1 being object st
( s1 in the carrier' of (MSSign (A,P)) & S2[s2,s1] )
proof
let s2 be
object ;
( s2 in the carrier' of S2 implies ex s1 being object st
( s1 in the carrier' of (MSSign (A,P)) & S2[s2,s1] ) )
assume
s2 in the
carrier' of
S2
;
ex s1 being object st
( s1 in the carrier' of (MSSign (A,P)) & S2[s2,s1] )
then reconsider s2 =
s2 as
OperSymbol of
S2 ;
SG * (the_arity_of s2) is
FinSequence of
rng R
by Lm2;
then consider p being
FinSequence of
P such that A16:
product (SG * (the_arity_of s2)) c= product p
by A1, Th3, Th26;
reconsider p =
p as
Element of
P * by FINSEQ_1:def 11;
take s1 =
[(Q -index_of s2),p];
( s1 in the carrier' of (MSSign (A,P)) & S2[s2,s1] )
reconsider o =
Q -index_of s2 as
OperSymbol of
A by A4, Def3;
set aa = the
Element of
Args (
s2,
G);
A17:
the
Element of
Args (
s2,
G)
in Args (
s2,
G)
;
A18:
dom (Den (s2,G)) = Args (
s2,
G)
by FUNCT_2:def 1;
A19:
dom the
Arity of
S2 = the
carrier' of
S2
by PARTFUN1:def 2;
A20:
dom the
Charact of
G = the
carrier' of
S2
by PARTFUN1:def 2;
the
Charact of
G | (Q . o) is
IndexedPartition of
Den (
o,
A)
by A2;
then
rng ( the Charact of G | (Q . o)) is
a_partition of
Den (
o,
A)
by Def2;
then A21:
the
Charact of
G .: (Q . o) is
a_partition of
Den (
o,
A)
by RELAT_1:115;
s2 in Q . o
by Def3;
then
the
Charact of
G . s2 in the
Charact of
G .: (Q . o)
by A20, FUNCT_1:def 6;
then A22:
dom (Den (s2,G)) c= dom (Den (o,A))
by A21, RELAT_1:11;
A23:
Args (
s2,
G) =
( the Sorts of G #) . ( the Arity of S2 . s2)
by A19, FUNCT_1:13
.=
product (SG * (the_arity_of s2))
by FINSEQ_2:def 5
;
then
product p meets dom (Den (o,A))
by A16, A17, A18, A22, XBOOLE_0:3;
hence
s1 in the
carrier' of
(MSSign (A,P))
by A6;
S2[s2,s1]
take
p
;
ex o being OperSymbol of S2 st
( s1 = [(Q -index_of s2),p] & s2 = o & Args (o,G) c= product p )
take
s2
;
( s1 = [(Q -index_of s2),p] & s2 = s2 & Args (s2,G) c= product p )
thus
(
s1 = [(Q -index_of s2),p] &
s2 = s2 &
Args (
s2,
G)
c= product p )
by A16, A23;
verum
end;
consider g being Function such that
A24:
( dom g = the carrier' of S2 & rng g c= the carrier' of (MSSign (A,P)) & ( for s being object st s in the carrier' of S2 holds
S2[s,g . s] ) )
from FUNCT_1:sch 6(A15);
reconsider g = g as Function of the carrier' of S2, the carrier' of (MSSign (A,P)) by A24, FUNCT_2:2;
take
g
; ( f,g form_morphism_between S2, MSSign (A,P) & rng f = the carrier of (MSSign (A,P)) & rng g = the carrier' of (MSSign (A,P)) )
thus A25:
( dom f = the carrier of S2 & dom g = the carrier' of S2 & rng f c= the carrier of (MSSign (A,P)) & rng g c= the carrier' of (MSSign (A,P)) )
by FUNCT_2:def 1; PUA2MSS1:def 12 ( f * the ResultSort of S2 = the ResultSort of (MSSign (A,P)) * g & ( for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f * p = the Arity of (MSSign (A,P)) . (g . o) ) & rng f = the carrier of (MSSign (A,P)) & rng g = the carrier' of (MSSign (A,P)) )
now for c being OperSymbol of S2 holds (f * the ResultSort of S2) . c = ( the ResultSort of (MSSign (A,P)) * g) . clet c be
OperSymbol of
S2;
(f * the ResultSort of S2) . c = ( the ResultSort of (MSSign (A,P)) * g) . cset s = the
ResultSort of
S2 . c;
A26:
R . ( the ResultSort of S2 . c) = ( the Sorts of G * the ResultSort of S2) . c
by FUNCT_2:15;
A27:
(f * the ResultSort of S2) . c = f . ( the ResultSort of S2 . c)
by FUNCT_2:15;
R . ( the ResultSort of S2 . c) in rng R
by A5, FUNCT_1:def 3;
then
S1[
R . ( the ResultSort of S2 . c),
em . (R . ( the ResultSort of S2 . c))]
by A12;
then
R . ( the ResultSort of S2 . c) c= em . (R . ( the ResultSort of S2 . c))
;
then A28:
R . ( the ResultSort of S2 . c) c= f . ( the ResultSort of S2 . c)
by A5, FUNCT_1:13;
consider p being
FinSequence of
P,
o being
OperSymbol of
S2 such that A29:
g . c = [(Q -index_of c),p]
and A30:
c = o
and A31:
Args (
o,
G)
c= product p
by A24;
reconsider p =
p as
Element of
P * by FINSEQ_1:def 11;
reconsider s2 =
Q -index_of c as
OperSymbol of
A by A4, Def3;
set aa = the
Element of
Args (
o,
G);
the
Charact of
G | (Q . s2) is
IndexedPartition of
Den (
s2,
A)
by A2;
then A32:
rng ( the Charact of G | (Q . s2)) is
a_partition of
Den (
s2,
A)
by Def2;
A33:
o in Q . s2
by A30, Def3;
A34:
dom the
Charact of
G = the
carrier' of
S2
by PARTFUN1:def 2;
A35:
the
Charact of
G .: (Q . s2) is
a_partition of
Den (
s2,
A)
by A32, RELAT_1:115;
A36:
the
Charact of
G . o in the
Charact of
G .: (Q . s2)
by A33, A34, FUNCT_1:def 6;
A37:
dom (Den (o,G)) = Args (
o,
G)
by FUNCT_2:def 1;
A38:
dom (Den (o,G)) c= dom (Den (s2,A))
by A35, A36, RELAT_1:11;
the
Element of
Args (
o,
G)
in Args (
o,
G)
;
then
product p meets dom (Den (s2,A))
by A31, A37, A38, XBOOLE_0:3;
then A39:
(Den (s2,A)) .: (product p) c= the
ResultSort of
(MSSign (A,P)) . (g . c)
by A29, Def14;
rng (Den (c,G)) = (Den (c,G)) .: (Args (c,G))
by A30, A37, RELAT_1:113;
then A40:
rng (Den (c,G)) c= (Den (c,G)) .: (product p)
by A30, A31, RELAT_1:123;
(Den (c,G)) .: (product p) c= (Den (s2,A)) .: (product p)
by A30, A35, A36, RELAT_1:124;
then
rng (Den (c,G)) c= (Den (s2,A)) .: (product p)
by A40;
then A41:
rng (Den (c,G)) c= the
ResultSort of
(MSSign (A,P)) . (g . c)
by A39;
A42:
(Den (c,G)) . the
Element of
Args (
o,
G)
in rng (Den (c,G))
by A30, A37, FUNCT_1:def 3;
then A43:
(Den (c,G)) . the
Element of
Args (
o,
G)
in ( the Sorts of G * the ResultSort of S2) . c
;
(Den (c,G)) . the
Element of
Args (
o,
G)
in the
ResultSort of
(MSSign (A,P)) . (g . c)
by A41, A42;
then
(Den (c,G)) . the
Element of
Args (
o,
G)
in ( the ResultSort of (MSSign (A,P)) * g) . c
by FUNCT_2:15;
hence
(f * the ResultSort of S2) . c = ( the ResultSort of (MSSign (A,P)) * g) . c
by A7, A26, A27, A28, A43, Lm3;
verum end;
hence
f * the ResultSort of S2 = the ResultSort of (MSSign (A,P)) * g
; ( ( for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f * p = the Arity of (MSSign (A,P)) . (g . o) ) & rng f = the carrier of (MSSign (A,P)) & rng g = the carrier' of (MSSign (A,P)) )
hereby ( rng f = the carrier of (MSSign (A,P)) & rng g = the carrier' of (MSSign (A,P)) )
let o be
set ;
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f * p = the Arity of (MSSign (A,P)) . (g . o)let p be
Function;
( o in the carrier' of S2 & p = the Arity of S2 . o implies f * p = the Arity of (MSSign (A,P)) . (g . o) )assume
o in the
carrier' of
S2
;
( p = the Arity of S2 . o implies f * p = the Arity of (MSSign (A,P)) . (g . o) )then reconsider s =
o as
OperSymbol of
S2 ;
assume A44:
p = the
Arity of
S2 . o
;
f * p = the Arity of (MSSign (A,P)) . (g . o)reconsider q = the
Arity of
S2 . s as
Element of the
carrier of
S2 * ;
reconsider r =
SG * q as
FinSequence of
rng R by Lm2;
consider p9 being
FinSequence of
P,
o9 being
OperSymbol of
S2 such that A45:
g . s = [(Q -index_of s),p9]
and A46:
s = o9
and A47:
Args (
o9,
G)
c= product p9
by A24;
g . s in the
carrier' of
(MSSign (A,P))
;
then consider o1 being
OperSymbol of
A,
p1 being
Element of
P * such that A48:
g . s = [o1,p1]
and A49:
product p1 meets dom (Den (o1,A))
by A6;
p9 = p1
by A45, A48, XTUPLE_0:1;
then A50:
the
Arity of
(MSSign (A,P)) . (g . o) = p9
by A48, A49, Def14;
Args (
o9,
G) =
( the Sorts of G #) . q
by A46, FUNCT_2:15
.=
product r
by FINSEQ_2:def 5
;
then A51:
product r c= product p9
by A47;
em * r = p9
by Th4, A51, A13;
hence
f * p = the
Arity of
(MSSign (A,P)) . (g . o)
by A44, A50, RELAT_1:36;
verum
end;
thus
rng f c= the carrier of (MSSign (A,P))
; XBOOLE_0:def 10 ( the carrier of (MSSign (A,P)) c= rng f & rng g = the carrier' of (MSSign (A,P)) )
thus
the carrier of (MSSign (A,P)) c= rng f
rng g = the carrier' of (MSSign (A,P))proof
let s be
object ;
TARSKI:def 3 ( not s in the carrier of (MSSign (A,P)) or s in rng f )
assume
s in the
carrier of
(MSSign (A,P))
;
s in rng f
then reconsider s =
s as
Element of
P by Def14;
set a = the
Element of
s;
A52:
R -index_of the
Element of
s in dom R
by Def3;
A53:
the
Element of
s in R . (R -index_of the Element of s)
by Def3;
A54:
R . (R -index_of the Element of s) in rng R
by A52, FUNCT_1:def 3;
A55:
em . (R . (R -index_of the Element of s)) = f . (R -index_of the Element of s)
by A52, FUNCT_1:13;
S1[
R . (R -index_of the Element of s),
em . (R . (R -index_of the Element of s))]
by A12, A54;
then A56:
R . (R -index_of the Element of s) c= f . (R -index_of the Element of s)
by A55;
A57:
f . (R -index_of the Element of s) in rng f
by A5, A25, A52, FUNCT_1:def 3;
rng f c= P
by A25, Def14;
hence
s in rng f
by A53, A56, A57, Lm3;
verum
end;
thus
rng g c= the carrier' of (MSSign (A,P))
; XBOOLE_0:def 10 the carrier' of (MSSign (A,P)) c= rng g
thus
the carrier' of (MSSign (A,P)) c= rng g
verumproof
let s1 be
object ;
TARSKI:def 3 ( not s1 in the carrier' of (MSSign (A,P)) or s1 in rng g )
assume
s1 in the
carrier' of
(MSSign (A,P))
;
s1 in rng g
then consider o being
OperSymbol of
A,
p being
Element of
P * such that A58:
s1 = [o,p]
and A59:
product p meets dom (Den (o,A))
by A6;
consider a being
object such that A60:
a in product p
and
a in dom (Den (o,A))
by A59, XBOOLE_0:3;
consider h being
Function such that A61:
a = h
and A62:
dom h = dom p
and A63:
for
x being
object st
x in dom p holds
h . x in p . x
by A60, CARD_3:def 5;
reconsider h =
h as
FinSequence by A62, Lm1;
product p c= Funcs (
(dom p),
(Union p))
by FUNCT_6:1;
then A64:
ex
f being
Function st
(
h = f &
dom f = dom p &
rng f c= Union p )
by A60, A61, FUNCT_2:def 2;
A65:
Union p = union (rng p)
by CARD_3:def 4;
A66:
union (rng p) c= union P
by ZFMISC_1:77;
union P = the
carrier of
A
by EQREL_1:def 4;
then
rng h c= the
carrier of
A
by A64, A65, A66;
then
h is
FinSequence of the
carrier of
A
by FINSEQ_1:def 4;
then consider r being
FinSequence of
rng R such that A67:
h in product r
by Th6;
A68:
dom h = dom r
by A67, CARD_3:9;
A69:
Den (
o,
A)
is_exactly_partitable_wrt P
by Def10;
now for x being object st x in dom r holds
r . x c= p . xlet x be
object ;
( x in dom r implies r . x c= p . x )assume A70:
x in dom r
;
r . x c= p . xthen A71:
h . x in p . x
by A62, A63, A68;
A72:
h . x in r . x
by A67, A70, CARD_3:9;
A73:
r . x in rng r
by A70, FUNCT_1:def 3;
A74:
p . x in rng p
by A62, A68, A70, FUNCT_1:def 3;
ex
c being
set st
(
c in P &
r . x c= c )
by A8, A73;
hence
r . x c= p . x
by A71, A72, A74, Lm3;
verum end;
then A75:
product r c= product p
by A62, A68, CARD_3:27;
product p c= dom (Den (o,A))
by A59, A69;
then consider s2 being
OperSymbol of
S2 such that A76:
the
Sorts of
G * (the_arity_of s2) = r
and A77:
s2 in Q . o
by A2, A75, Th31, XBOOLE_1:1;
consider p9 being
FinSequence of
P,
o9 being
OperSymbol of
S2 such that A78:
g . s2 = [(Q -index_of s2),p9]
and A79:
s2 = o9
and A80:
Args (
o9,
G)
c= product p9
by A24;
dom the
Arity of
S2 = the
carrier' of
S2
by FUNCT_2:def 1;
then Args (
s2,
G) =
( the Sorts of G #) . ( the Arity of S2 . s2)
by FUNCT_1:13
.=
product r
by A76, FINSEQ_2:def 5
;
then A81:
p9 = em * r
by A13, A79, A80, Th4;
A82:
p = em * r
by A13, A75, Th4;
Q -index_of s2 = o
by A4, A77, Def3;
hence
s1 in rng g
by A24, A58, A78, A81, A82, FUNCT_1:def 3;
verum
end;