let A be partial non-empty UAStr ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: ( 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 ; :: according to PUA2MSS1:def 16 :: thesis: 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] )
proof
let r be object ; :: thesis: ( r in rng R implies ex p being object st
( p in P & S1[r,p] ) )
assume A10: r in rng R ; :: thesis: ex p being object st
( p in P & S1[r,p] )
reconsider r = r as set by TARSKI:1;
ex p being set st
( p in P & r c= p ) by A10, A8;
hence ex p being object st
( p in P & S1[r,p] ) ; :: thesis: verum
end;
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
proof
let a be set ; :: thesis: ( a in rng R implies a c= em . a )
assume a in rng R ; :: thesis: a c= em . a
then S1[a,em . a] by A12;
hence a c= em . a ; :: thesis: verum
end;
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 ; :: according to PUA2MSS1:def 13 :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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]; :: thesis: ( 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; :: thesis: S2[s2,s1]
take p ; :: thesis: ex o being OperSymbol of S2 st
( s1 = [(Q -index_of s2),p] & s2 = o & Args (o,G) c= product p )
take s2 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: according to PUA2MSS1:def 12 :: thesis: ( 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 :: thesis: for c being OperSymbol of S2 holds (f * the ResultSort of S2) . c = ( the ResultSort of (MSSign (A,P)) * g) . c
let c be OperSymbol of S2; :: thesis: (f * the ResultSort of S2) . c = ( the ResultSort of (MSSign (A,P)) * g) . c
set 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; :: thesis: verum
end;
hence f * the ResultSort of S2 = the ResultSort of (MSSign (A,P)) * g ; :: thesis: ( ( 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 :: thesis: ( rng f = the carrier of (MSSign (A,P)) & rng g = the carrier' of (MSSign (A,P)) )
let o be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
thus rng f c= the carrier of (MSSign (A,P)) ; :: according to XBOOLE_0:def 10 :: thesis: ( 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 :: thesis: rng g = the carrier' of (MSSign (A,P))
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in the carrier of (MSSign (A,P)) or s in rng f )
assume s in the carrier of (MSSign (A,P)) ; :: thesis: 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; :: thesis: verum
end;
thus rng g c= the carrier' of (MSSign (A,P)) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of (MSSign (A,P)) c= rng g
thus the carrier' of (MSSign (A,P)) c= rng g :: thesis: verum
proof
let s1 be object ; :: according to TARSKI:def 3 :: thesis: ( not s1 in the carrier' of (MSSign (A,P)) or s1 in rng g )
assume s1 in the carrier' of (MSSign (A,P)) ; :: thesis: 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 :: thesis: for x being object st x in dom r holds
r . x c= p . x
let x be object ; :: thesis: ( x in dom r implies r . x c= p . x )
assume A70: x in dom r ; :: thesis: r . x c= p . x
then 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; :: thesis: 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; :: thesis: verum
end;