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 of S2, Q being IndexedPartition of the carrier' of S2 such that A2:
A can_be_characterized_by S2,G,Q
; PUA2MSS1:def 17 MSSign (A,P) is_rougher_than S2
A3:
the Sorts of G is IndexedPartition of A
by A2, Def16;
A4:
dom Q = dom the charact of A
by A2, Def16;
reconsider G = G as non-empty MSAlgebra of S2 by A3, MSUALG_1:def 8;
reconsider R = the Sorts of G as IndexedPartition of A by A2, Def16;
A5:
dom R = the carrier of S2
by PARTFUN1:def 4;
then reconsider SG = the Sorts of G as Function of the carrier of S2,(rng R) by RELSET_1:11;
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 Def15;
A7:
the carrier of (MSSign (A,P)) = P
by Def15;
defpred S1[ set , set ] means $1 c= $2;
A8:
rng R is_finer_than P
by A1, Th28;
then A9:
for r being set st r in rng R holds
ex p being set st
( p in P & S1[r,p] )
by SETFAM_1:def 2;
consider em being Function such that
A10:
( dom em = rng R & rng em c= P )
and
A11:
for r being set st r in rng R holds
S1[r,em . r]
from WELLORD2:sch 1(A9);
reconsider em = em as Function of (rng R),P by A10, FUNCT_2:4;
A12:
dom (em * R) = dom R
by A10, RELAT_1:46;
rng (em * R) = rng em
by A10, RELAT_1:47;
then reconsider f = em * R as Function of the carrier of S2, the carrier of (MSSign (A,P)) by A5, A7, A12, FUNCT_2:4;
take
f
; PUA2MSS1:def 14 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[ set , set ] 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 );
A13:
for s2 being set st s2 in the carrier' of S2 holds
ex s1 being set st
( s1 in the carrier' of (MSSign (A,P)) & S2[s2,s1] )
proof
let s2 be
set ;
( s2 in the carrier' of S2 implies ex s1 being set st
( s1 in the carrier' of (MSSign (A,P)) & S2[s2,s1] ) )
assume
s2 in the
carrier' of
S2
;
ex s1 being set 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 A14:
product (SG * (the_arity_of s2)) c= product p
by A1, Th4, Th28;
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, Def4;
consider aa being
Element of
Args (
s2,
G);
A15:
aa in Args (
s2,
G)
;
A16:
dom (Den (s2,G)) = Args (
s2,
G)
by FUNCT_2:def 1;
A17:
dom the
Arity of
S2 = the
carrier' of
S2
by PARTFUN1:def 4;
A18:
dom the
Charact of
G = the
carrier' of
S2
by PARTFUN1:def 4;
the
Charact of
G | (Q . o) is
IndexedPartition of
Den (
o,
A)
by A2, Def16;
then
rng ( the Charact of G | (Q . o)) is
a_partition of
Den (
o,
A)
by Def3;
then A19:
the
Charact of
G .: (Q . o) is
a_partition of
Den (
o,
A)
by RELAT_1:148;
s2 in Q . o
by Def4;
then
the
Charact of
G . s2 in the
Charact of
G .: (Q . o)
by A18, FUNCT_1:def 12;
then A20:
dom (Den (s2,G)) c= dom (Den (o,A))
by A19, RELAT_1:25;
A21:
Args (
s2,
G) =
( the Sorts of G #) . ( the Arity of S2 . s2)
by A17, FUNCT_1:23
.=
product (SG * (the_arity_of s2))
by PBOOLE:def 19
;
then
product p meets dom (Den (o,A))
by A14, A15, A16, A20, 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 A14, A21;
verum
end;
consider g being Function such that
A22:
( dom g = the carrier' of S2 & rng g c= the carrier' of (MSSign (A,P)) & ( for s being set st s in the carrier' of S2 holds
S2[s,g . s] ) )
from WELLORD2:sch 1(A13);
reconsider g = g as Function of the carrier' of S2, the carrier' of (MSSign (A,P)) by A22, FUNCT_2:4;
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 A23:
( 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 13 ( 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 let 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;
A24:
R . ( the ResultSort of S2 . c) = ( the Sorts of G * the ResultSort of S2) . c
by FUNCT_2:21;
A25:
(f * the ResultSort of S2) . c = f . ( the ResultSort of S2 . c)
by FUNCT_2:21;
R . ( the ResultSort of S2 . c) in rng R
by A5, FUNCT_1:def 5;
then
R . ( the ResultSort of S2 . c) c= em . (R . ( the ResultSort of S2 . c))
by A11;
then A26:
R . ( the ResultSort of S2 . c) c= f . ( the ResultSort of S2 . c)
by A5, FUNCT_1:23;
consider p being
FinSequence of
P,
o being
OperSymbol of
S2 such that A27:
g . c = [(Q -index_of c),p]
and A28:
c = o
and A29:
Args (
o,
G)
c= product p
by A22;
reconsider p =
p as
Element of
P * by FINSEQ_1:def 11;
reconsider s2 =
Q -index_of c as
OperSymbol of
A by A4, Def4;
consider aa being
Element of
Args (
o,
G);
the
Charact of
G | (Q . s2) is
IndexedPartition of
Den (
s2,
A)
by A2, Def16;
then A30:
rng ( the Charact of G | (Q . s2)) is
a_partition of
Den (
s2,
A)
by Def3;
A31:
o in Q . s2
by A28, Def4;
A32:
dom the
Charact of
G = the
carrier' of
S2
by PARTFUN1:def 4;
A33:
the
Charact of
G .: (Q . s2) is
a_partition of
Den (
s2,
A)
by A30, RELAT_1:148;
A34:
the
Charact of
G . o in the
Charact of
G .: (Q . s2)
by A31, A32, FUNCT_1:def 12;
A35:
dom (Den (o,G)) = Args (
o,
G)
by FUNCT_2:def 1;
A36:
dom (Den (o,G)) c= dom (Den (s2,A))
by A33, A34, RELAT_1:25;
aa in Args (
o,
G)
;
then
product p meets dom (Den (s2,A))
by A29, A35, A36, XBOOLE_0:3;
then A37:
(Den (s2,A)) .: (product p) c= the
ResultSort of
(MSSign (A,P)) . (g . c)
by A27, Def15;
rng (Den (c,G)) = (Den (c,G)) .: (Args (c,G))
by A28, A35, RELAT_1:146;
then A38:
rng (Den (c,G)) c= (Den (c,G)) .: (product p)
by A28, A29, RELAT_1:156;
(Den (c,G)) .: (product p) c= (Den (s2,A)) .: (product p)
by A28, A33, A34, RELAT_1:157;
then
rng (Den (c,G)) c= (Den (s2,A)) .: (product p)
by A38, XBOOLE_1:1;
then A39:
rng (Den (c,G)) c= the
ResultSort of
(MSSign (A,P)) . (g . c)
by A37, XBOOLE_1:1;
A40:
(Den (c,G)) . aa in rng (Den (c,G))
by A28, A35, FUNCT_1:def 5;
then A41:
(Den (c,G)) . aa in ( the Sorts of G * the ResultSort of S2) . c
;
(Den (c,G)) . aa in the
ResultSort of
(MSSign (A,P)) . (g . c)
by A39, A40;
then
(Den (c,G)) . aa in ( the ResultSort of (MSSign (A,P)) * g) . c
by FUNCT_2:21;
hence
(f * the ResultSort of S2) . c = ( the ResultSort of (MSSign (A,P)) * g) . c
by A7, A24, A25, A26, A41, Th3;
verum end;
hence
f * the ResultSort of S2 = the ResultSort of (MSSign (A,P)) * g
by FUNCT_2:113; ( ( 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 A42:
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 A43:
g . s = [(Q -index_of s),p9]
and A44:
s = o9
and A45:
Args (
o9,
G)
c= product p9
by A22;
g . s in the
carrier' of
(MSSign (A,P))
;
then consider o1 being
OperSymbol of
A,
p1 being
Element of
P * such that A46:
g . s = [o1,p1]
and A47:
product p1 meets dom (Den (o1,A))
by A6;
p9 = p1
by A43, A46, ZFMISC_1:33;
then A48:
the
Arity of
(MSSign (A,P)) . (g . o) = p9
by A46, A47, Def15;
Args (
o9,
G) =
( the Sorts of G #) . q
by A44, FUNCT_2:21
.=
product r
by PBOOLE:def 19
;
then
em * r = p9
by A11, A45, Th5;
hence
f * p = the
Arity of
(MSSign (A,P)) . (g . o)
by A42, A48, RELAT_1:55;
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
set ;
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 Def15;
consider a being
Element of
s;
A49:
R -index_of a in dom R
by Def4;
A50:
a in R . (R -index_of a)
by Def4;
A51:
R . (R -index_of a) in rng R
by A49, FUNCT_1:def 5;
em . (R . (R -index_of a)) = f . (R -index_of a)
by A49, FUNCT_1:23;
then A52:
R . (R -index_of a) c= f . (R -index_of a)
by A11, A51;
A53:
f . (R -index_of a) in rng f
by A5, A23, A49, FUNCT_1:def 5;
rng f c= P
by A23, Def15;
hence
s in rng f
by A50, A52, A53, Th3;
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
set ;
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 A54:
s1 = [o,p]
and A55:
product p meets dom (Den (o,A))
by A6;
consider a being
set such that A56:
a in product p
and
a in dom (Den (o,A))
by A55, XBOOLE_0:3;
consider h being
Function such that A57:
a = h
and A58:
dom h = dom p
and A59:
for
x being
set st
x in dom p holds
h . x in p . x
by A56, CARD_3:def 5;
reconsider h =
h as
FinSequence by A58, Lm1;
product p c= Funcs (
(dom p),
(Union p))
by FUNCT_6:10;
then A60:
ex
f being
Function st
(
h = f &
dom f = dom p &
rng f c= Union p )
by A56, A57, FUNCT_2:def 2;
A61:
Union p = union (rng p)
by CARD_3:def 4;
A62:
union (rng p) c= union P
by ZFMISC_1:95;
union P = the
carrier of
A
by EQREL_1:def 6;
then
rng h c= the
carrier of
A
by A60, A61, A62, XBOOLE_1:1;
then
h is
FinSequence of the
carrier of
A
by FINSEQ_1:def 4;
then consider r being
FinSequence of
rng R such that A63:
h in product r
by Th7;
A64:
dom h = dom r
by A63, CARD_3:18;
A65:
Den (
o,
A)
is_exactly_partitable_wrt P
by Def11;
now let x be
set ;
( x in dom r implies r . x c= p . x )assume A66:
x in dom r
;
r . x c= p . xthen A67:
h . x in p . x
by A58, A59, A64;
A68:
h . x in r . x
by A63, A66, CARD_3:18;
A69:
r . x in rng r
by A66, FUNCT_1:def 5;
A70:
p . x in rng p
by A58, A64, A66, FUNCT_1:def 5;
ex
c being
set st
(
c in P &
r . x c= c )
by A8, A69, SETFAM_1:def 2;
hence
r . x c= p . x
by A67, A68, A70, Th3;
verum end;
then A71:
product r c= product p
by A58, A64, CARD_3:38;
product p c= dom (Den (o,A))
by A55, A65, Def10;
then consider s2 being
OperSymbol of
S2 such that A72:
the
Sorts of
G * (the_arity_of s2) = r
and A73:
s2 in Q . o
by A2, A71, Th33, XBOOLE_1:1;
consider p9 being
FinSequence of
P,
o9 being
OperSymbol of
S2 such that A74:
g . s2 = [(Q -index_of s2),p9]
and A75:
s2 = o9
and A76:
Args (
o9,
G)
c= product p9
by A22;
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:23
.=
product r
by A72, PBOOLE:def 19
;
then A77:
p9 = em * r
by A11, A75, A76, Th5;
A78:
p = em * r
by A11, A71, Th5;
Q -index_of s2 = o
by A4, A73, Def4;
hence
s1 in rng g
by A22, A54, A74, A77, A78, FUNCT_1:def 5;
verum
end;