:: PUA2MSS1 semantic presentation
begin
Lm1: for p being FinSequence
for f being Function st dom f = dom p holds
f is FinSequence
proof
let p be FinSequence; ::_thesis: for f being Function st dom f = dom p holds
f is FinSequence
dom p = Seg (len p) by FINSEQ_1:def_3;
hence for f being Function st dom f = dom p holds
f is FinSequence by FINSEQ_1:def_2; ::_thesis: verum
end;
Lm2: for X being set
for Y being non empty set
for p being FinSequence of X
for f being Function of X,Y holds f * p is FinSequence of Y
proof
let X be set ; ::_thesis: for Y being non empty set
for p being FinSequence of X
for f being Function of X,Y holds f * p is FinSequence of Y
let Y be non empty set ; ::_thesis: for p being FinSequence of X
for f being Function of X,Y holds f * p is FinSequence of Y
let p be FinSequence of X; ::_thesis: for f being Function of X,Y holds f * p is FinSequence of Y
let f be Function of X,Y; ::_thesis: f * p is FinSequence of Y
A1: rng p c= X ;
dom f = X by FUNCT_2:def_1;
then dom (f * p) = dom p by A1, RELAT_1:27;
then A2: f * p is FinSequence by Lm1;
rng (f * p) c= Y ;
hence f * p is FinSequence of Y by A2, FINSEQ_1:def_4; ::_thesis: verum
end;
registration
let X be with_non-empty_elements set ;
cluster -> non-empty for FinSequence of X;
coherence
for b1 being FinSequence of X holds b1 is non-empty
proof
let p be FinSequence of X; ::_thesis: p is non-empty
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in proj1 p or not p . x is empty )
assume x in dom p ; ::_thesis: not p . x is empty
then p . x in rng p by FUNCT_1:def_3;
hence not p . x is empty ; ::_thesis: verum
end;
end;
registration
let A be non empty set ;
cluster non empty Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued Function-like V44() FinSequence-like FinSubsequence-like countable homogeneous quasi_total for FinSequence of PFuncs ((A *),A);
existence
ex b1 being PFuncFinSequence of A st
( b1 is homogeneous & b1 is quasi_total & b1 is non-empty & not b1 is empty )
proof
set a = the non empty homogeneous quasi_total PartFunc of (A *),A;
reconsider a = the non empty homogeneous quasi_total PartFunc of (A *),A as Element of PFuncs ((A *),A) by PARTFUN1:45;
take <*a*> ; ::_thesis: ( <*a*> is homogeneous & <*a*> is quasi_total & <*a*> is non-empty & not <*a*> is empty )
hereby :: according to MARGREL1:def_23 ::_thesis: ( <*a*> is quasi_total & <*a*> is non-empty & not <*a*> is empty )
let n be Nat; ::_thesis: for h being PartFunc of (A *),A st n in dom <*a*> & h = <*a*> . n holds
h is homogeneous
let h be PartFunc of (A *),A; ::_thesis: ( n in dom <*a*> & h = <*a*> . n implies h is homogeneous )
assume n in dom <*a*> ; ::_thesis: ( h = <*a*> . n implies h is homogeneous )
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def_1;
hence ( h = <*a*> . n implies h is homogeneous ) by FINSEQ_1:40; ::_thesis: verum
end;
hereby :: according to MARGREL1:def_24 ::_thesis: ( <*a*> is non-empty & not <*a*> is empty )
let n be Nat; ::_thesis: for h being PartFunc of (A *),A st n in dom <*a*> & h = <*a*> . n holds
h is quasi_total
let h be PartFunc of (A *),A; ::_thesis: ( n in dom <*a*> & h = <*a*> . n implies h is quasi_total )
assume n in dom <*a*> ; ::_thesis: ( h = <*a*> . n implies h is quasi_total )
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def_1;
hence ( h = <*a*> . n implies h is quasi_total ) by FINSEQ_1:40; ::_thesis: verum
end;
hereby :: according to FUNCT_1:def_9 ::_thesis: not <*a*> is empty
let n be set ; ::_thesis: ( n in dom <*a*> implies not <*a*> . n is empty )
assume n in dom <*a*> ; ::_thesis: not <*a*> . n is empty
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def_1;
hence not <*a*> . n is empty by FINSEQ_1:40; ::_thesis: verum
end;
thus not <*a*> is empty ; ::_thesis: verum
end;
end;
registration
cluster non-empty -> non empty for UAStr ;
coherence
for b1 being UAStr st b1 is non-empty holds
not b1 is empty
proof
let A be UAStr ; ::_thesis: ( A is non-empty implies not A is empty )
assume that
A1: the charact of A <> {} and
A2: the charact of A is non-empty ; :: according to UNIALG_1:def_3 ::_thesis: not A is empty
reconsider f = the charact of A as non empty Function by A1;
set x = the Element of dom f;
reconsider y = f . the Element of dom f as non empty set by A2;
A3: y in rng f by FUNCT_1:def_3;
rng f c= PFuncs (( the carrier of A *), the carrier of A) by FINSEQ_1:def_4;
then A4: y is PartFunc of ( the carrier of A *), the carrier of A by A3, PARTFUN1:47;
reconsider y = y as non empty Function ;
thus not the carrier of A is empty by A4; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
theorem Th1: :: PUA2MSS1:1
for f, g being non-empty Function st product f c= product g holds
( dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) )
proof
let f, g be non-empty Function; ::_thesis: ( product f c= product g implies ( dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) ) )
assume A1: product f c= product g ; ::_thesis: ( dom f = dom g & ( for x being set st x in dom f holds
f . x c= g . x ) )
set h = the Element of product f;
the Element of product f in product f ;
then A2: ex i being Function st
( the Element of product f = i & dom i = dom g & ( for x being set st x in dom g holds
i . x in g . x ) ) by A1, CARD_3:def_5;
A3: ex i being Function st
( the Element of product f = i & dom i = dom f & ( for x being set st x in dom f holds
i . x in f . x ) ) by CARD_3:def_5;
hence dom f = dom g by A2; ::_thesis: for x being set st x in dom f holds
f . x c= g . x
let x be set ; ::_thesis: ( x in dom f implies f . x c= g . x )
assume A4: x in dom f ; ::_thesis: f . x c= g . x
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in f . x or z in g . x )
set k = the Element of product f;
reconsider k = the Element of product f as Function ;
defpred S1[ set ] means $1 = x;
deffunc H1( set ) -> set = z;
deffunc H2( set ) -> set = k . $1;
consider h being Function such that
A5: ( dom h = dom f & ( for y being set st y in dom f holds
( ( S1[y] implies h . y = H1(y) ) & ( not S1[y] implies h . y = H2(y) ) ) ) ) from PARTFUN1:sch_1();
assume A6: z in f . x ; ::_thesis: z in g . x
now__::_thesis:_for_y_being_set_st_y_in_dom_f_holds_
h_._y_in_f_._y
let y be set ; ::_thesis: ( y in dom f implies h . y in f . y )
assume A7: y in dom f ; ::_thesis: h . y in f . y
then ( y <> x implies h . y = k . y ) by A5;
hence h . y in f . y by A5, A6, A7, CARD_3:9; ::_thesis: verum
end;
then h in product f by A5, CARD_3:9;
then h . x in g . x by A1, A2, A3, A4, CARD_3:9;
hence z in g . x by A4, A5; ::_thesis: verum
end;
theorem Th2: :: PUA2MSS1:2
for f, g being non-empty Function st product f = product g holds
f = g
proof
let f, g be non-empty Function; ::_thesis: ( product f = product g implies f = g )
assume A1: product f = product g ; ::_thesis: f = g
set h = the Element of product f;
A2: ex i being Function st
( the Element of product f = i & dom i = dom g & ( for x being set st x in dom g holds
i . x in g . x ) ) by A1, CARD_3:def_5;
A3: ex i being Function st
( the Element of product f = i & dom i = dom f & ( for x being set st x in dom f holds
i . x in f . x ) ) by CARD_3:def_5;
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A4: x in dom f ; ::_thesis: f . x = g . x
then A5: f . x c= g . x by A1, Th1;
g . x c= f . x by A1, A2, A3, A4, Th1;
hence f . x = g . x by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
hence f = g by A2, A3, FUNCT_1:2; ::_thesis: verum
end;
definition
let A be non empty set ;
let f be PFuncFinSequence of A;
:: original: proj2
redefine func rng f -> Subset of (PFuncs ((A *),A));
coherence
proj2 f is Subset of (PFuncs ((A *),A)) by FINSEQ_1:def_4;
end;
definition
let A, B be non empty set ;
let S be non empty Subset of (PFuncs (A,B));
:: original: Element
redefine mode Element of S -> PartFunc of A,B;
coherence
for b1 being Element of S holds b1 is PartFunc of A,B
proof
let s be Element of S; ::_thesis: s is PartFunc of A,B
thus s is PartFunc of A,B by PARTFUN1:46; ::_thesis: verum
end;
end;
definition
let A be non-empty UAStr ;
mode OperSymbol of A is Element of dom the charact of A;
mode operation of A is Element of rng the charact of A;
end;
definition
let A be non-empty UAStr ;
let o be OperSymbol of A;
func Den (o,A) -> operation of A equals :: PUA2MSS1:def 1
the charact of A . o;
correctness
coherence
the charact of A . o is operation of A;
by FUNCT_1:def_3;
end;
:: deftheorem defines Den PUA2MSS1:def_1_:_
for A being non-empty UAStr
for o being OperSymbol of A holds Den (o,A) = the charact of A . o;
begin
theorem :: PUA2MSS1:3
canceled;
Lm3: for X being set
for P being a_partition of X
for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
by EQREL_1:70;
theorem Th4: :: PUA2MSS1:4
for X, Y being set st X is_finer_than Y holds
for p being FinSequence of X ex q being FinSequence of Y st product p c= product q
proof
let X, Y be set ; ::_thesis: ( X is_finer_than Y implies for p being FinSequence of X ex q being FinSequence of Y st product p c= product q )
assume A1: for a being set st a in X holds
ex b being set st
( b in Y & a c= b ) ; :: according to SETFAM_1:def_2 ::_thesis: for p being FinSequence of X ex q being FinSequence of Y st product p c= product q
let p be FinSequence of X; ::_thesis: ex q being FinSequence of Y st product p c= product q
defpred S1[ set , set ] means p . $1 c= $2;
A2: for i being set st i in dom p holds
ex y being set st
( y in Y & S1[i,y] )
proof
let i be set ; ::_thesis: ( i in dom p implies ex y being set st
( y in Y & S1[i,y] ) )
assume i in dom p ; ::_thesis: ex y being set st
( y in Y & S1[i,y] )
then p . i in rng p by FUNCT_1:def_3;
hence ex y being set st
( y in Y & S1[i,y] ) by A1; ::_thesis: verum
end;
consider q being Function such that
A3: ( dom q = dom p & rng q c= Y & ( for i being set st i in dom p holds
S1[i,q . i] ) ) from FUNCT_1:sch_5(A2);
dom p = Seg (len p) by FINSEQ_1:def_3;
then q is FinSequence by A3, FINSEQ_1:def_2;
then A4: q is FinSequence of Y by A3, FINSEQ_1:def_4;
product p c= product q by A3, CARD_3:27;
hence ex q being FinSequence of Y st product p c= product q by A4; ::_thesis: verum
end;
theorem Th5: :: PUA2MSS1:5
for X being set
for P, Q being a_partition of X
for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
proof
let X be set ; ::_thesis: for P, Q being a_partition of X
for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let P, Q be a_partition of X; ::_thesis: for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let f be Function of P,Q; ::_thesis: ( ( for a being set st a in P holds
a c= f . a ) implies for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q ) )
assume A1: for a being set st a in P holds
a c= f . a ; ::_thesis: for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let p be FinSequence of P; ::_thesis: for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let q be FinSequence of Q; ::_thesis: ( product p c= product q iff f * p = q )
A2: rng p c= P ;
now__::_thesis:_(_P_<>_{}_implies_Q_<>_{}_)
assume P <> {} ; ::_thesis: Q <> {}
then reconsider X = X as non empty set by EQREL_1:32;
Q is a_partition of X ;
hence Q <> {} ; ::_thesis: verum
end;
then dom f = P by FUNCT_2:def_1;
then A3: dom (f * p) = dom p by A2, RELAT_1:27;
hereby ::_thesis: ( f * p = q implies product p c= product q )
assume A4: product p c= product q ; ::_thesis: f * p = q
then A5: dom p = dom q by Th1;
now__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_
(f_*_p)_._x_=_q_._x
let x be set ; ::_thesis: ( x in dom p implies (f * p) . x = q . x )
assume A6: x in dom p ; ::_thesis: (f * p) . x = q . x
then A7: p . x c= q . x by A4, Th1;
A8: p . x in rng p by A6, FUNCT_1:def_3;
A9: q . x in rng q by A5, A6, FUNCT_1:def_3;
reconsider Y = X as non empty set by A8, EQREL_1:32;
reconsider P9 = P, Q9 = Q as a_partition of Y ;
reconsider a = p . x as Element of P9 by A8;
set z = the Element of a;
A10: a c= f . a by A1;
A11: the Element of a in a ;
f . a in Q9 by FUNCT_2:5;
then q . x = f . a by A7, A9, A10, A11, Lm3;
hence (f * p) . x = q . x by A6, FUNCT_1:13; ::_thesis: verum
end;
hence f * p = q by A3, A5, FUNCT_1:2; ::_thesis: verum
end;
assume A12: f * p = q ; ::_thesis: product p c= product q
now__::_thesis:_for_x_being_set_st_x_in_dom_p_holds_
p_._x_c=_q_._x
let x be set ; ::_thesis: ( x in dom p implies p . x c= q . x )
assume A13: x in dom p ; ::_thesis: p . x c= q . x
then A14: q . x = f . (p . x) by A12, FUNCT_1:13;
p . x in rng p by A13, FUNCT_1:def_3;
hence p . x c= q . x by A1, A14; ::_thesis: verum
end;
hence product p c= product q by A3, A12, CARD_3:27; ::_thesis: verum
end;
theorem Th6: :: PUA2MSS1:6
for P being set
for f being Function st rng f c= union P holds
ex p being Function st
( dom p = dom f & rng p c= P & f in product p )
proof
let P be set ; ::_thesis: for f being Function st rng f c= union P holds
ex p being Function st
( dom p = dom f & rng p c= P & f in product p )
let f be Function; ::_thesis: ( rng f c= union P implies ex p being Function st
( dom p = dom f & rng p c= P & f in product p ) )
assume A1: rng f c= union P ; ::_thesis: ex p being Function st
( dom p = dom f & rng p c= P & f in product p )
defpred S1[ set , set ] means f . $1 in $2;
A2: for x being set st x in dom f holds
ex a being set st
( a in P & S1[x,a] )
proof
let x be set ; ::_thesis: ( x in dom f implies ex a being set st
( a in P & S1[x,a] ) )
assume x in dom f ; ::_thesis: ex a being set st
( a in P & S1[x,a] )
then f . x in rng f by FUNCT_1:def_3;
then ex a being set st
( f . x in a & a in P ) by A1, TARSKI:def_4;
hence ex a being set st
( a in P & S1[x,a] ) ; ::_thesis: verum
end;
consider p being Function such that
A3: ( dom p = dom f & rng p c= P ) and
A4: for x being set st x in dom f holds
S1[x,p . x] from FUNCT_1:sch_5(A2);
take p ; ::_thesis: ( dom p = dom f & rng p c= P & f in product p )
thus ( dom p = dom f & rng p c= P & f in product p ) by A3, A4, CARD_3:def_5; ::_thesis: verum
end;
theorem Th7: :: PUA2MSS1:7
for X being set
for P being a_partition of X
for f being FinSequence of X ex p being FinSequence of P st f in product p
proof
let X be set ; ::_thesis: for P being a_partition of X
for f being FinSequence of X ex p being FinSequence of P st f in product p
let P be a_partition of X; ::_thesis: for f being FinSequence of X ex p being FinSequence of P st f in product p
let f be FinSequence of X; ::_thesis: ex p being FinSequence of P st f in product p
A1: rng f c= X ;
union P = X by EQREL_1:def_4;
then consider p being Function such that
A2: dom p = dom f and
A3: rng p c= P and
A4: f in product p by A1, Th6;
dom p = Seg (len f) by A2, FINSEQ_1:def_3;
then p is FinSequence by FINSEQ_1:def_2;
then p is FinSequence of P by A3, FINSEQ_1:def_4;
hence ex p being FinSequence of P st f in product p by A4; ::_thesis: verum
end;
theorem :: PUA2MSS1:8
for X, Y being non empty set
for P being a_partition of X
for Q being a_partition of Y holds { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:]
proof
let X, Y be non empty set ; ::_thesis: for P being a_partition of X
for Q being a_partition of Y holds { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:]
let P be a_partition of X; ::_thesis: for Q being a_partition of Y holds { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:]
let Q be a_partition of Y; ::_thesis: { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:]
set PQ = { [:p,q:] where p is Element of P, q is Element of Q : verum } ;
{ [:p,q:] where p is Element of P, q is Element of Q : verum } c= bool [:X,Y:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [:p,q:] where p is Element of P, q is Element of Q : verum } or x in bool [:X,Y:] )
assume x in { [:p,q:] where p is Element of P, q is Element of Q : verum } ; ::_thesis: x in bool [:X,Y:]
then ex p being Element of P ex q being Element of Q st x = [:p,q:] ;
hence x in bool [:X,Y:] ; ::_thesis: verum
end;
then reconsider PQ = { [:p,q:] where p is Element of P, q is Element of Q : verum } as Subset-Family of [:X,Y:] ;
PQ is a_partition of [:X,Y:]
proof
thus union PQ = [:X,Y:] :: according to EQREL_1:def_4 ::_thesis: for b1 being Element of bool [:X,Y:] holds
( not b1 in PQ or ( not b1 = {} & ( for b2 being Element of bool [:X,Y:] holds
( not b2 in PQ or b1 = b2 or b1 misses b2 ) ) ) )
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in union PQ or [x,y] in [:X,Y:] ) & ( not [x,y] in [:X,Y:] or [x,y] in union PQ ) )
thus ( [x,y] in union PQ implies [x,y] in [:X,Y:] ) ; ::_thesis: ( not [x,y] in [:X,Y:] or [x,y] in union PQ )
assume A1: [x,y] in [:X,Y:] ; ::_thesis: [x,y] in union PQ
then A2: x in X by ZFMISC_1:87;
A3: y in Y by A1, ZFMISC_1:87;
X = union P by EQREL_1:def_4;
then consider p being set such that
A4: x in p and
A5: p in P by A2, TARSKI:def_4;
Y = union Q by EQREL_1:def_4;
then consider q being set such that
A6: y in q and
A7: q in Q by A3, TARSKI:def_4;
A8: [x,y] in [:p,q:] by A4, A6, ZFMISC_1:87;
[:p,q:] in PQ by A5, A7;
hence [x,y] in union PQ by A8, TARSKI:def_4; ::_thesis: verum
end;
let A be Subset of [:X,Y:]; ::_thesis: ( not A in PQ or ( not A = {} & ( for b1 being Element of bool [:X,Y:] holds
( not b1 in PQ or A = b1 or A misses b1 ) ) ) )
assume A in PQ ; ::_thesis: ( not A = {} & ( for b1 being Element of bool [:X,Y:] holds
( not b1 in PQ or A = b1 or A misses b1 ) ) )
then consider p being Element of P, q being Element of Q such that
A9: A = [:p,q:] ;
thus A <> {} by A9; ::_thesis: for b1 being Element of bool [:X,Y:] holds
( not b1 in PQ or A = b1 or A misses b1 )
let B be Subset of [:X,Y:]; ::_thesis: ( not B in PQ or A = B or A misses B )
assume B in PQ ; ::_thesis: ( A = B or A misses B )
then consider p1 being Element of P, q1 being Element of Q such that
A10: B = [:p1,q1:] ;
assume A <> B ; ::_thesis: A misses B
then ( p <> p1 or q <> q1 ) by A9, A10;
then ( p misses p1 or q misses q1 ) by EQREL_1:def_4;
then ( p /\ p1 = {} or q /\ q1 = {} ) by XBOOLE_0:def_7;
then ( A /\ B = [:{},(q /\ q1):] or A /\ B = [:(p /\ p1),{}:] ) by A9, A10, ZFMISC_1:100;
then A /\ B = {} by ZFMISC_1:90;
hence A misses B by XBOOLE_0:def_7; ::_thesis: verum
end;
hence { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:] ; ::_thesis: verum
end;
theorem Th9: :: PUA2MSS1:9
for X being non empty set
for P being a_partition of X holds { (product p) where p is Element of P * : verum } is a_partition of X *
proof
let X be non empty set ; ::_thesis: for P being a_partition of X holds { (product p) where p is Element of P * : verum } is a_partition of X *
let P be a_partition of X; ::_thesis: { (product p) where p is Element of P * : verum } is a_partition of X *
set PP = { (product p) where p is Element of P * : verum } ;
{ (product p) where p is Element of P * : verum } c= bool (X *)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (product p) where p is Element of P * : verum } or x in bool (X *) )
assume x in { (product p) where p is Element of P * : verum } ; ::_thesis: x in bool (X *)
then consider p being Element of P * such that
A1: x = product p ;
x c= X *
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in X * )
assume y in x ; ::_thesis: y in X *
then consider f being Function such that
A2: y = f and
A3: dom f = dom p and
A4: for z being set st z in dom p holds
f . z in p . z by A1, CARD_3:def_5;
dom p = Seg (len p) by FINSEQ_1:def_3;
then A5: y is FinSequence by A2, A3, FINSEQ_1:def_2;
rng f c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in X )
assume z in rng f ; ::_thesis: z in X
then consider v being set such that
A6: v in dom p and
A7: z = f . v by A3, FUNCT_1:def_3;
p . v in rng p by A6, FUNCT_1:def_3;
then A8: p . v in P ;
z in p . v by A4, A6, A7;
hence z in X by A8; ::_thesis: verum
end;
then y is FinSequence of X by A2, A5, FINSEQ_1:def_4;
hence y in X * by FINSEQ_1:def_11; ::_thesis: verum
end;
hence x in bool (X *) ; ::_thesis: verum
end;
then reconsider PP = { (product p) where p is Element of P * : verum } as Subset-Family of (X *) ;
PP is a_partition of X *
proof
thus union PP c= X * ; :: according to XBOOLE_0:def_10,EQREL_1:def_4 ::_thesis: ( X * c= union PP & ( for b1 being Element of bool (X *) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (X *) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) ) ) )
thus X * c= union PP ::_thesis: for b1 being Element of bool (X *) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (X *) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X * or x in union PP )
assume x in X * ; ::_thesis: x in union PP
then reconsider x = x as FinSequence of X by FINSEQ_1:def_11;
A9: rng x c= X ;
union P = X by EQREL_1:def_4;
then consider p being Function such that
A10: dom p = dom x and
A11: rng p c= P and
A12: x in product p by A9, Th6;
dom p = Seg (len x) by A10, FINSEQ_1:def_3;
then reconsider p = p as FinSequence by FINSEQ_1:def_2;
reconsider p = p as FinSequence of P by A11, FINSEQ_1:def_4;
reconsider p = p as Element of P * by FINSEQ_1:def_11;
product p in PP ;
hence x in union PP by A12, TARSKI:def_4; ::_thesis: verum
end;
let A be Subset of (X *); ::_thesis: ( not A in PP or ( not A = {} & ( for b1 being Element of bool (X *) holds
( not b1 in PP or A = b1 or A misses b1 ) ) ) )
assume A in PP ; ::_thesis: ( not A = {} & ( for b1 being Element of bool (X *) holds
( not b1 in PP or A = b1 or A misses b1 ) ) )
then consider p being Element of P * such that
A13: A = product p ;
thus A <> {} by A13; ::_thesis: for b1 being Element of bool (X *) holds
( not b1 in PP or A = b1 or A misses b1 )
let B be Subset of (X *); ::_thesis: ( not B in PP or A = B or A misses B )
assume B in PP ; ::_thesis: ( A = B or A misses B )
then consider q being Element of P * such that
A14: B = product q ;
assume A15: A <> B ; ::_thesis: A misses B
assume A meets B ; ::_thesis: contradiction
then consider x being set such that
A16: x in A and
A17: x in B by XBOOLE_0:3;
consider f being Function such that
A18: x = f and
A19: dom f = dom p and
A20: for z being set st z in dom p holds
f . z in p . z by A13, A16, CARD_3:def_5;
A21: ex g being Function st
( x = g & dom g = dom q & ( for z being set st z in dom q holds
g . z in q . z ) ) by A14, A17, CARD_3:def_5;
now__::_thesis:_for_z_being_set_st_z_in_dom_p_holds_
p_._z_=_q_._z
let z be set ; ::_thesis: ( z in dom p implies p . z = q . z )
assume A22: z in dom p ; ::_thesis: p . z = q . z
then A23: f . z in p . z by A20;
A24: f . z in q . z by A18, A19, A21, A22;
A25: p . z in rng p by A22, FUNCT_1:def_3;
A26: q . z in rng q by A18, A19, A21, A22, FUNCT_1:def_3;
A27: p . z meets q . z by A23, A24, XBOOLE_0:3;
A28: p . z in P by A25;
q . z in P by A26;
hence p . z = q . z by A27, A28, EQREL_1:def_4; ::_thesis: verum
end;
hence contradiction by A13, A14, A15, A18, A19, A21, FUNCT_1:2; ::_thesis: verum
end;
hence { (product p) where p is Element of P * : verum } is a_partition of X * ; ::_thesis: verum
end;
theorem :: PUA2MSS1:10
for X being non empty set
for n being Element of NAT
for P being a_partition of X holds { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
proof
let X be non empty set ; ::_thesis: for n being Element of NAT
for P being a_partition of X holds { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
let n be Element of NAT ; ::_thesis: for P being a_partition of X holds { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
let P be a_partition of X; ::_thesis: { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X
set nP = n -tuples_on P;
set nX = n -tuples_on X;
set PP = { (product p) where p is Element of n -tuples_on P : verum } ;
{ (product p) where p is Element of n -tuples_on P : verum } c= bool (n -tuples_on X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (product p) where p is Element of n -tuples_on P : verum } or x in bool (n -tuples_on X) )
assume x in { (product p) where p is Element of n -tuples_on P : verum } ; ::_thesis: x in bool (n -tuples_on X)
then consider p being Element of n -tuples_on P such that
A1: x = product p ;
x c= n -tuples_on X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in n -tuples_on X )
assume y in x ; ::_thesis: y in n -tuples_on X
then consider f being Function such that
A2: y = f and
A3: dom f = dom p and
A4: for z being set st z in dom p holds
f . z in p . z by A1, CARD_3:def_5;
A5: dom p = Seg (len p) by FINSEQ_1:def_3;
then reconsider y = y as FinSequence by A2, A3, FINSEQ_1:def_2;
rng f c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in X )
assume z in rng f ; ::_thesis: z in X
then consider v being set such that
A6: v in dom p and
A7: z = f . v by A3, FUNCT_1:def_3;
p . v in rng p by A6, FUNCT_1:def_3;
then A8: p . v in P ;
z in p . v by A4, A6, A7;
hence z in X by A8; ::_thesis: verum
end;
then A9: y is FinSequence of X by A2, FINSEQ_1:def_4;
A10: len y = len p by A2, A3, A5, FINSEQ_1:def_3;
len p = n by CARD_1:def_7;
then y is Element of n -tuples_on X by A9, A10, FINSEQ_2:92;
hence y in n -tuples_on X ; ::_thesis: verum
end;
hence x in bool (n -tuples_on X) ; ::_thesis: verum
end;
then reconsider PP = { (product p) where p is Element of n -tuples_on P : verum } as Subset-Family of (n -tuples_on X) ;
PP is a_partition of n -tuples_on X
proof
thus union PP c= n -tuples_on X ; :: according to XBOOLE_0:def_10,EQREL_1:def_4 ::_thesis: ( n -tuples_on X c= union PP & ( for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (n -tuples_on X) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) ) ) )
thus n -tuples_on X c= union PP ::_thesis: for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or ( not b1 = {} & ( for b2 being Element of bool (n -tuples_on X) holds
( not b2 in PP or b1 = b2 or b1 misses b2 ) ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n -tuples_on X or x in union PP )
assume x in n -tuples_on X ; ::_thesis: x in union PP
then reconsider x = x as Element of n -tuples_on X ;
A11: rng x c= X ;
union P = X by EQREL_1:def_4;
then consider p being Function such that
A12: dom p = dom x and
A13: rng p c= P and
A14: x in product p by A11, Th6;
A15: dom p = Seg (len x) by A12, FINSEQ_1:def_3;
then reconsider p = p as FinSequence by FINSEQ_1:def_2;
reconsider p = p as FinSequence of P by A13, FINSEQ_1:def_4;
A16: len p = len x by A15, FINSEQ_1:def_3;
len x = n by CARD_1:def_7;
then reconsider p = p as Element of n -tuples_on P by A16, FINSEQ_2:92;
product p in PP ;
hence x in union PP by A14, TARSKI:def_4; ::_thesis: verum
end;
let A be Subset of (n -tuples_on X); ::_thesis: ( not A in PP or ( not A = {} & ( for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or A = b1 or A misses b1 ) ) ) )
assume A in PP ; ::_thesis: ( not A = {} & ( for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or A = b1 or A misses b1 ) ) )
then consider p being Element of n -tuples_on P such that
A17: A = product p ;
thus A <> {} by A17; ::_thesis: for b1 being Element of bool (n -tuples_on X) holds
( not b1 in PP or A = b1 or A misses b1 )
let B be Subset of (n -tuples_on X); ::_thesis: ( not B in PP or A = B or A misses B )
assume B in PP ; ::_thesis: ( A = B or A misses B )
then consider q being Element of n -tuples_on P such that
A18: B = product q ;
assume A19: A <> B ; ::_thesis: A misses B
assume A meets B ; ::_thesis: contradiction
then consider x being set such that
A20: x in A and
A21: x in B by XBOOLE_0:3;
consider f being Function such that
A22: x = f and
A23: dom f = dom p and
A24: for z being set st z in dom p holds
f . z in p . z by A17, A20, CARD_3:def_5;
A25: ex g being Function st
( x = g & dom g = dom q & ( for z being set st z in dom q holds
g . z in q . z ) ) by A18, A21, CARD_3:def_5;
now__::_thesis:_for_z_being_set_st_z_in_dom_p_holds_
p_._z_=_q_._z
let z be set ; ::_thesis: ( z in dom p implies p . z = q . z )
assume A26: z in dom p ; ::_thesis: p . z = q . z
then A27: f . z in p . z by A24;
A28: f . z in q . z by A22, A23, A25, A26;
A29: p . z in rng p by A26, FUNCT_1:def_3;
A30: q . z in rng q by A22, A23, A25, A26, FUNCT_1:def_3;
A31: p . z meets q . z by A27, A28, XBOOLE_0:3;
A32: p . z in P by A29;
q . z in P by A30;
hence p . z = q . z by A31, A32, EQREL_1:def_4; ::_thesis: verum
end;
hence contradiction by A17, A18, A19, A22, A23, A25, FUNCT_1:2; ::_thesis: verum
end;
hence { (product p) where p is Element of n -tuples_on P : verum } is a_partition of n -tuples_on X ; ::_thesis: verum
end;
theorem Th11: :: PUA2MSS1:11
for X being non empty set
for Y being set st Y c= X holds
for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
proof
let X be non empty set ; ::_thesis: for Y being set st Y c= X holds
for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
let Y be set ; ::_thesis: ( Y c= X implies for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y )
assume A1: Y c= X ; ::_thesis: for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
let P be a_partition of X; ::_thesis: { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
set Q = { (a /\ Y) where a is Element of P : a meets Y } ;
{ (a /\ Y) where a is Element of P : a meets Y } c= bool Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (a /\ Y) where a is Element of P : a meets Y } or x in bool Y )
assume x in { (a /\ Y) where a is Element of P : a meets Y } ; ::_thesis: x in bool Y
then ex p being Element of P st
( x = p /\ Y & p meets Y ) ;
then A2: x c= X /\ Y by XBOOLE_1:26;
X /\ Y = Y by A1, XBOOLE_1:28;
hence x in bool Y by A2; ::_thesis: verum
end;
then reconsider Q = { (a /\ Y) where a is Element of P : a meets Y } as Subset-Family of Y ;
Q is a_partition of Y
proof
thus union Q c= Y ; :: according to XBOOLE_0:def_10,EQREL_1:def_4 ::_thesis: ( Y c= union Q & ( for b1 being Element of bool Y holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) ) ) )
thus Y c= union Q ::_thesis: for b1 being Element of bool Y holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in union Q )
assume A3: x in Y ; ::_thesis: x in union Q
X = union P by EQREL_1:def_4;
then consider p being set such that
A4: x in p and
A5: p in P by A1, A3, TARSKI:def_4;
A6: p meets Y by A3, A4, XBOOLE_0:3;
A7: x in p /\ Y by A3, A4, XBOOLE_0:def_4;
p /\ Y in Q by A5, A6;
hence x in union Q by A7, TARSKI:def_4; ::_thesis: verum
end;
let A be Subset of Y; ::_thesis: ( not A in Q or ( not A = {} & ( for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 ) ) ) )
assume A in Q ; ::_thesis: ( not A = {} & ( for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 ) ) )
then consider p being Element of P such that
A8: A = p /\ Y and
A9: p meets Y ;
thus A <> {} by A8, A9, XBOOLE_0:def_7; ::_thesis: for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 )
let B be Subset of Y; ::_thesis: ( not B in Q or A = B or A misses B )
assume B in Q ; ::_thesis: ( A = B or A misses B )
then consider p1 being Element of P such that
A10: B = p1 /\ Y and
p1 meets Y ;
assume A <> B ; ::_thesis: A misses B
then p misses p1 by A8, A10, EQREL_1:def_4;
then A misses p1 by A8, XBOOLE_1:74;
hence A misses B by A10, XBOOLE_1:74; ::_thesis: verum
end;
hence { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y ; ::_thesis: verum
end;
theorem Th12: :: PUA2MSS1:12
for f being non empty Function
for P being a_partition of dom f holds { (f | a) where a is Element of P : verum } is a_partition of f
proof
let f be non empty Function; ::_thesis: for P being a_partition of dom f holds { (f | a) where a is Element of P : verum } is a_partition of f
set X = dom f;
let P be a_partition of dom f; ::_thesis: { (f | a) where a is Element of P : verum } is a_partition of f
set Y = f;
set Q = { (f | a) where a is Element of P : verum } ;
{ (f | a) where a is Element of P : verum } c= bool f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f | a) where a is Element of P : verum } or x in bool f )
assume x in { (f | a) where a is Element of P : verum } ; ::_thesis: x in bool f
then ex p being Element of P st x = f | p ;
then x c= f by RELAT_1:59;
hence x in bool f ; ::_thesis: verum
end;
then reconsider Q = { (f | a) where a is Element of P : verum } as Subset-Family of f ;
Q is a_partition of f
proof
f c= union Q
proof
let y, z be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [y,z] in f or [y,z] in union Q )
assume A1: [y,z] in f ; ::_thesis: [y,z] in union Q
then A2: y in dom f by XTUPLE_0:def_12;
dom f = union P by EQREL_1:def_4;
then consider p being set such that
A3: y in p and
A4: p in P by A2, TARSKI:def_4;
A5: [y,z] in f | p by A1, A3, RELAT_1:def_11;
f | p in Q by A4;
hence [y,z] in union Q by A5, TARSKI:def_4; ::_thesis: verum
end;
hence f = union Q by XBOOLE_0:def_10; :: according to EQREL_1:def_4 ::_thesis: for b1 being Element of bool f holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool f holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) )
let A be Subset of f; ::_thesis: ( not A in Q or ( not A = {} & ( for b1 being Element of bool f holds
( not b1 in Q or A = b1 or A misses b1 ) ) ) )
assume A in Q ; ::_thesis: ( not A = {} & ( for b1 being Element of bool f holds
( not b1 in Q or A = b1 or A misses b1 ) ) )
then consider p being Element of P such that
A6: A = f | p ;
reconsider p = p as non empty Subset of (dom f) ;
thus A <> {} by A6; ::_thesis: for b1 being Element of bool f holds
( not b1 in Q or A = b1 or A misses b1 )
let B be Subset of f; ::_thesis: ( not B in Q or A = B or A misses B )
assume B in Q ; ::_thesis: ( A = B or A misses B )
then consider p1 being Element of P such that
A7: B = f | p1 ;
assume A <> B ; ::_thesis: A misses B
then A8: p misses p1 by A6, A7, EQREL_1:def_4;
assume A meets B ; ::_thesis: contradiction
then consider x being set such that
A9: x in A and
A10: x in B by XBOOLE_0:3;
consider y, z being set such that
A11: x = [y,z] by A9, RELAT_1:def_1;
A12: y in p by A6, A9, A11, RELAT_1:def_11;
y in p1 by A7, A10, A11, RELAT_1:def_11;
hence contradiction by A8, A12, XBOOLE_0:3; ::_thesis: verum
end;
hence { (f | a) where a is Element of P : verum } is a_partition of f ; ::_thesis: verum
end;
theorem Th13: :: PUA2MSS1:13
for X being set
for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}
proof
let X be set ; ::_thesis: for p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q}
set P = SmallestPartition X;
let p be FinSequence of SmallestPartition X; ::_thesis: ex q being FinSequence of X st product p = {q}
set q = the Element of product p;
A1: dom the Element of product p = dom p by CARD_3:9;
then reconsider q = the Element of product p as FinSequence by Lm1;
A2: q in product p ;
A3: product p c= Funcs ((dom p),(Union p)) by FUNCT_6:1;
A4: Union p = union (rng p) by CARD_3:def_4;
A5: ex f being Function st
( q = f & dom f = dom p & rng f c= Union p ) by A2, A3, FUNCT_2:def_2;
Union p c= union (SmallestPartition X) by A4, ZFMISC_1:77;
then rng q c= union (SmallestPartition X) by A5, XBOOLE_1:1;
then rng q c= X by EQREL_1:def_4;
then reconsider q = q as FinSequence of X by FINSEQ_1:def_4;
take q ; ::_thesis: product p = {q}
thus product p c= {q} :: according to XBOOLE_0:def_10 ::_thesis: {q} c= product p
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product p or x in {q} )
assume x in product p ; ::_thesis: x in {q}
then consider g being Function such that
A6: x = g and
A7: dom g = dom p and
A8: for x being set st x in dom p holds
g . x in p . x by CARD_3:def_5;
now__::_thesis:_for_y_being_set_st_y_in_dom_p_holds_
g_._y_=_q_._y
let y be set ; ::_thesis: ( y in dom p implies g . y = q . y )
assume A9: y in dom p ; ::_thesis: g . y = q . y
then A10: g . y in p . y by A8;
A11: q . y in p . y by A9, CARD_3:9;
A12: p . y in rng p by A9, FUNCT_1:def_3;
then A13: p . y in SmallestPartition X ;
reconsider X = X as non empty set by A12, EQREL_1:32;
SmallestPartition X = { {z} where z is Element of X : verum } by EQREL_1:37;
then consider z being Element of X such that
A14: p . y = {z} by A13;
thus g . y = z by A10, A14, TARSKI:def_1
.= q . y by A11, A14, TARSKI:def_1 ; ::_thesis: verum
end;
then x = q by A1, A6, A7, FUNCT_1:2;
hence x in {q} by TARSKI:def_1; ::_thesis: verum
end;
thus {q} c= product p by ZFMISC_1:31; ::_thesis: verum
end;
definition
let X be set ;
mode IndexedPartition of X -> Function means :Def2: :: PUA2MSS1:def 2
( rng it is a_partition of X & it is one-to-one );
existence
ex b1 being Function st
( rng b1 is a_partition of X & b1 is one-to-one )
proof
set p = the a_partition of X;
take id the a_partition of X ; ::_thesis: ( rng (id the a_partition of X) is a_partition of X & id the a_partition of X is one-to-one )
thus ( rng (id the a_partition of X) is a_partition of X & id the a_partition of X is one-to-one ) ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines IndexedPartition PUA2MSS1:def_2_:_
for X being set
for b2 being Function holds
( b2 is IndexedPartition of X iff ( rng b2 is a_partition of X & b2 is one-to-one ) );
definition
let X be set ;
let P be IndexedPartition of X;
:: original: proj2
redefine func rng P -> a_partition of X;
coherence
proj2 P is a_partition of X by Def2;
end;
registration
let X be set ;
cluster -> non-empty one-to-one for IndexedPartition of X;
coherence
for b1 being IndexedPartition of X holds
( b1 is one-to-one & b1 is non-empty )
proof
let P be IndexedPartition of X; ::_thesis: ( P is one-to-one & P is non-empty )
thus P is one-to-one by Def2; ::_thesis: P is non-empty
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in proj1 P or not P . x is empty )
assume x in dom P ; ::_thesis: not P . x is empty
then P . x in rng P by FUNCT_1:def_3;
hence not P . x is empty ; ::_thesis: verum
end;
end;
registration
let X be non empty set ;
cluster -> non empty for IndexedPartition of X;
coherence
for b1 being IndexedPartition of X holds not b1 is empty
proof
let P be IndexedPartition of X; ::_thesis: not P is empty
set a = the Element of rng P;
ex b being set st [b, the Element of rng P] in P by XTUPLE_0:def_13;
hence not P is empty ; ::_thesis: verum
end;
end;
definition
let X be set ;
let P be a_partition of X;
:: original: id
redefine func id P -> IndexedPartition of X;
coherence
id P is IndexedPartition of X
proof
rng (id P) = P ;
hence id P is IndexedPartition of X by Def2; ::_thesis: verum
end;
end;
definition
let X be set ;
let P be IndexedPartition of X;
let x be set ;
assume A1: x in X ;
A2: union (rng P) = X by EQREL_1:def_4;
funcP -index_of x -> set means :Def3: :: PUA2MSS1:def 3
( it in dom P & x in P . it );
existence
ex b1 being set st
( b1 in dom P & x in P . b1 )
proof
consider a being set such that
A3: x in a and
A4: a in rng P by A1, A2, TARSKI:def_4;
ex y being set st
( y in dom P & a = P . y ) by A4, FUNCT_1:def_3;
hence ex b1 being set st
( b1 in dom P & x in P . b1 ) by A3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being set st b1 in dom P & x in P . b1 & b2 in dom P & x in P . b2 holds
b1 = b2;
proof
let y1, y2 be set ; ::_thesis: ( y1 in dom P & x in P . y1 & y2 in dom P & x in P . y2 implies y1 = y2 )
assume that
A5: y1 in dom P and
A6: x in P . y1 and
A7: y2 in dom P and
A8: x in P . y2 ; ::_thesis: y1 = y2
A9: P . y1 in rng P by A5, FUNCT_1:def_3;
A10: P . y2 in rng P by A7, FUNCT_1:def_3;
P . y1 meets P . y2 by A6, A8, XBOOLE_0:3;
then P . y1 = P . y2 by A9, A10, EQREL_1:def_4;
hence y1 = y2 by A5, A7, FUNCT_1:def_4; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines -index_of PUA2MSS1:def_3_:_
for X being set
for P being IndexedPartition of X
for x being set st x in X holds
for b4 being set holds
( b4 = P -index_of x iff ( b4 in dom P & x in P . b4 ) );
theorem Th14: :: PUA2MSS1:14
for X being set
for P being non-empty Function st Union P = X & ( for x, y being set st x in dom P & y in dom P & x <> y holds
P . x misses P . y ) holds
P is IndexedPartition of X
proof
let X be set ; ::_thesis: for P being non-empty Function st Union P = X & ( for x, y being set st x in dom P & y in dom P & x <> y holds
P . x misses P . y ) holds
P is IndexedPartition of X
let P be non-empty Function; ::_thesis: ( Union P = X & ( for x, y being set st x in dom P & y in dom P & x <> y holds
P . x misses P . y ) implies P is IndexedPartition of X )
assume that
A1: Union P = X and
A2: for x, y being set st x in dom P & y in dom P & x <> y holds
P . x misses P . y ; ::_thesis: P is IndexedPartition of X
rng P c= bool X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng P or y in bool X )
assume y in rng P ; ::_thesis: y in bool X
then y c= union (rng P) by ZFMISC_1:74;
then y c= X by A1, CARD_3:def_4;
hence y in bool X ; ::_thesis: verum
end;
then reconsider Y = rng P as Subset-Family of X ;
Y is a_partition of X
proof
thus union Y = X by A1, CARD_3:def_4; :: according to EQREL_1:def_4 ::_thesis: for b1 being Element of bool X holds
( not b1 in Y or ( not b1 = {} & ( for b2 being Element of bool X holds
( not b2 in Y or b1 = b2 or b1 misses b2 ) ) ) )
let A be Subset of X; ::_thesis: ( not A in Y or ( not A = {} & ( for b1 being Element of bool X holds
( not b1 in Y or A = b1 or A misses b1 ) ) ) )
assume A3: A in Y ; ::_thesis: ( not A = {} & ( for b1 being Element of bool X holds
( not b1 in Y or A = b1 or A misses b1 ) ) )
then A4: ex x being set st
( x in dom P & A = P . x ) by FUNCT_1:def_3;
thus A <> {} by A3; ::_thesis: for b1 being Element of bool X holds
( not b1 in Y or A = b1 or A misses b1 )
let B be Subset of X; ::_thesis: ( not B in Y or A = B or A misses B )
assume B in Y ; ::_thesis: ( A = B or A misses B )
then ex y being set st
( y in dom P & B = P . y ) by FUNCT_1:def_3;
hence ( A = B or A misses B ) by A2, A4; ::_thesis: verum
end;
hence rng P is a_partition of X ; :: according to PUA2MSS1:def_2 ::_thesis: P is one-to-one
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in proj1 P or not y in proj1 P or not P . x = P . y or x = y )
assume that
A5: x in dom P and
A6: y in dom P and
A7: P . x = P . y and
A8: x <> y ; ::_thesis: contradiction
reconsider Px = P . x, Py = P . y as non empty set by A5, A6, FUNCT_1:def_9;
set a = the Element of Px;
P . x misses P . y by A2, A5, A6, A8;
then not the Element of Px in Py by XBOOLE_0:3;
hence contradiction by A7; ::_thesis: verum
end;
theorem Th15: :: PUA2MSS1:15
for X, Y being non empty set
for P being a_partition of Y
for f being Function of X,P st P c= rng f & f is one-to-one holds
f is IndexedPartition of Y
proof
let X, Y be non empty set ; ::_thesis: for P being a_partition of Y
for f being Function of X,P st P c= rng f & f is one-to-one holds
f is IndexedPartition of Y
let P be a_partition of Y; ::_thesis: for f being Function of X,P st P c= rng f & f is one-to-one holds
f is IndexedPartition of Y
let f be Function of X,P; ::_thesis: ( P c= rng f & f is one-to-one implies f is IndexedPartition of Y )
assume P c= rng f ; ::_thesis: ( not f is one-to-one or f is IndexedPartition of Y )
then rng f = P by XBOOLE_0:def_10;
hence ( not f is one-to-one or f is IndexedPartition of Y ) by Def2; ::_thesis: verum
end;
begin
scheme :: PUA2MSS1:sch 1
IndRelationEx{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of NAT , F4() -> Relation of F1(),F2(), F5( set , set ) -> Relation of F1(),F2() } :
ex R being Relation of F1(),F2() ex F being ManySortedSet of NAT st
( R = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) )
proof
deffunc H1( set , set ) -> Relation of F1(),F2() = F5($2,$1);
consider F being Function such that
A1: dom F = NAT and
A2: ( F . 0 = F4() & ( for n being Nat holds F . (n + 1) = H1(n,F . n) ) ) from NAT_1:sch_11();
reconsider F = F as ManySortedSet of NAT by A1, PARTFUN1:def_2, RELAT_1:def_18;
defpred S1[ Element of NAT ] means F . $1 is Relation of F1(),F2();
A3: S1[ 0 ] by A2;
A4: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume S1[i] ; ::_thesis: S1[i + 1]
then reconsider R = F . i as Relation of F1(),F2() ;
F . (i + 1) = F5(R,i) by A2;
hence S1[i + 1] ; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A3, A4);
then reconsider R = F . F3() as Relation of F1(),F2() ;
take R ; ::_thesis: ex F being ManySortedSet of NAT st
( R = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) )
take F ; ::_thesis: ( R = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) )
thus ( R = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) by A2; ::_thesis: verum
end;
scheme :: PUA2MSS1:sch 2
RelationUniq{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } :
for R1, R2 being Relation of F1(),F2() st ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R1 iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R2 iff P1[x,y] ) ) holds
R1 = R2
proof
let R1, R2 be Relation of F1(),F2(); ::_thesis: ( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R1 iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R2 iff P1[x,y] ) ) implies R1 = R2 )
assume that
A1: for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R1 iff P1[x,y] ) and
A2: for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R2 iff P1[x,y] ) ; ::_thesis: R1 = R2
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
hereby ::_thesis: ( not [x,y] in R2 or [x,y] in R1 )
assume A3: [x,y] in R1 ; ::_thesis: [x,y] in R2
then reconsider a = x as Element of F1() by ZFMISC_1:87;
reconsider b = y as Element of F2() by A3, ZFMISC_1:87;
P1[a,b] by A1, A3;
hence [x,y] in R2 by A2; ::_thesis: verum
end;
assume A4: [x,y] in R2 ; ::_thesis: [x,y] in R1
then reconsider a = x as Element of F1() by ZFMISC_1:87;
reconsider b = y as Element of F2() by A4, ZFMISC_1:87;
P1[a,b] by A2, A4;
hence [x,y] in R1 by A1; ::_thesis: verum
end;
scheme :: PUA2MSS1:sch 3
IndRelationUniq{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of NAT , F4() -> Relation of F1(),F2(), F5( set , set ) -> Relation of F1(),F2() } :
for R1, R2 being Relation of F1(),F2() st ex F being ManySortedSet of NAT st
( R1 = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) & ex F being ManySortedSet of NAT st
( R2 = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) holds
R1 = R2
proof
let R1, R2 be Relation of F1(),F2(); ::_thesis: ( ex F being ManySortedSet of NAT st
( R1 = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) & ex F being ManySortedSet of NAT st
( R2 = F . F3() & F . 0 = F4() & ( for i being Element of NAT
for R being Relation of F1(),F2() st R = F . i holds
F . (i + 1) = F5(R,i) ) ) implies R1 = R2 )
given F1 being ManySortedSet of NAT such that A1: R1 = F1 . F3() and
A2: F1 . 0 = F4() and
A3: for i being Element of NAT
for R being Relation of F1(),F2() st R = F1 . i holds
F1 . (i + 1) = F5(R,i) ; ::_thesis: ( for F being ManySortedSet of NAT holds
( not R2 = F . F3() or not F . 0 = F4() or ex i being Element of NAT ex R being Relation of F1(),F2() st
( R = F . i & not F . (i + 1) = F5(R,i) ) ) or R1 = R2 )
given F2 being ManySortedSet of NAT such that A4: R2 = F2 . F3() and
A5: F2 . 0 = F4() and
A6: for i being Element of NAT
for R being Relation of F1(),F2() st R = F2 . i holds
F2 . (i + 1) = F5(R,i) ; ::_thesis: R1 = R2
defpred S1[ Element of NAT ] means ( F1 . $1 = F2 . $1 & F1 . $1 is Relation of F1(),F2() );
A7: S1[ 0 ] by A2, A5;
A8: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; ::_thesis: S1[i + 1]
then reconsider R = F1 . i as Relation of F1(),F2() ;
F1 . (i + 1) = F5(R,i) by A3;
hence S1[i + 1] by A6, A9; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A7, A8);
hence R1 = R2 by A1, A4; ::_thesis: verum
end;
definition
let A be partial non-empty UAStr ;
func DomRel A -> Relation of the carrier of A means :Def4: :: PUA2MSS1:def 4
for x, y being Element of A holds
( [x,y] in it iff for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) );
existence
ex b1 being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in b1 iff for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) )
proof
defpred S1[ set , set ] means for f being operation of A
for p, q being FinSequence holds
( (p ^ <*$1*>) ^ q in dom f iff (p ^ <*$2*>) ^ q in dom f );
thus ex D being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in D iff S1[x,y] ) from RELSET_1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in b1 iff for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) ) & ( for x, y being Element of A holds
( [x,y] in b2 iff for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) ) holds
b1 = b2
proof
defpred S1[ set , set ] means for f being operation of A
for p, q being FinSequence holds
( (p ^ <*$1*>) ^ q in dom f iff (p ^ <*$2*>) ^ q in dom f );
thus for D1, D2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in D1 iff S1[x,y] ) ) & ( for x, y being Element of A holds
( [x,y] in D2 iff S1[x,y] ) ) holds
D1 = D2 from PUA2MSS1:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def4 defines DomRel PUA2MSS1:def_4_:_
for A being partial non-empty UAStr
for b2 being Relation of the carrier of A holds
( b2 = DomRel A iff for x, y being Element of A holds
( [x,y] in b2 iff for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) ) );
registration
let A be partial non-empty UAStr ;
cluster DomRel A -> total symmetric transitive ;
coherence
( DomRel A is total & DomRel A is symmetric & DomRel A is transitive )
proof
set X = the carrier of A;
A1: DomRel A is_reflexive_in the carrier of A
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of A or [x,x] in DomRel A )
for f being operation of A
for a, b being FinSequence holds
( (a ^ <*x*>) ^ b in dom f iff (a ^ <*x*>) ^ b in dom f ) ;
hence ( not x in the carrier of A or [x,x] in DomRel A ) by Def4; ::_thesis: verum
end;
then A2: dom (DomRel A) = the carrier of A by ORDERS_1:13;
A3: field (DomRel A) = the carrier of A by A1, ORDERS_1:13;
thus DomRel A is total by A2, PARTFUN1:def_2; ::_thesis: ( DomRel A is symmetric & DomRel A is transitive )
DomRel A is_symmetric_in the carrier of A
proof
let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in the carrier of A or not y in the carrier of A or not [x,y] in DomRel A or [y,x] in DomRel A )
assume that
A4: x in the carrier of A and
A5: y in the carrier of A ; ::_thesis: ( not [x,y] in DomRel A or [y,x] in DomRel A )
reconsider x9 = x, y9 = y as Element of the carrier of A by A4, A5;
assume [x,y] in DomRel A ; ::_thesis: [y,x] in DomRel A
then for f being operation of A
for a, b being FinSequence holds
( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*y9*>) ^ b in dom f ) by Def4;
hence [y,x] in DomRel A by Def4; ::_thesis: verum
end;
hence DomRel A is symmetric by A3, RELAT_2:def_11; ::_thesis: DomRel A is transitive
DomRel A is_transitive_in the carrier of A
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of A or not y in the carrier of A or not z in the carrier of A or not [x,y] in DomRel A or not [y,z] in DomRel A or [x,z] in DomRel A )
assume that
A6: x in the carrier of A and
A7: y in the carrier of A and
A8: z in the carrier of A ; ::_thesis: ( not [x,y] in DomRel A or not [y,z] in DomRel A or [x,z] in DomRel A )
reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of A by A6, A7, A8;
assume that
A9: [x,y] in DomRel A and
A10: [y,z] in DomRel A ; ::_thesis: [x,z] in DomRel A
now__::_thesis:_for_f_being_operation_of_A
for_a,_b_being_FinSequence_holds_
(_(a_^_<*x9*>)_^_b_in_dom_f_iff_(a_^_<*z9*>)_^_b_in_dom_f_)
let f be operation of A; ::_thesis: for a, b being FinSequence holds
( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*z9*>) ^ b in dom f )
let a, b be FinSequence; ::_thesis: ( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*z9*>) ^ b in dom f )
( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*y9*>) ^ b in dom f ) by A9, Def4;
hence ( (a ^ <*x9*>) ^ b in dom f iff (a ^ <*z9*>) ^ b in dom f ) by A10, Def4; ::_thesis: verum
end;
hence [x,z] in DomRel A by Def4; ::_thesis: verum
end;
hence DomRel A is transitive by A3, RELAT_2:def_16; ::_thesis: verum
end;
end;
definition
let A be partial non-empty UAStr ;
let R be Relation of the carrier of A;
funcR |^ A -> Relation of the carrier of A means :Def5: :: PUA2MSS1:def 5
for x, y being Element of A holds
( [x,y] in it iff ( [x,y] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in R ) ) );
existence
ex b1 being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in b1 iff ( [x,y] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in R ) ) )
proof
defpred S1[ set , set ] means ( [$1,$2] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*$1*>) ^ q in dom f & (p ^ <*$2*>) ^ q in dom f holds
[(f . ((p ^ <*$1*>) ^ q)),(f . ((p ^ <*$2*>) ^ q))] in R ) );
thus ex D being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in D iff S1[x,y] ) from RELSET_1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in b1 iff ( [x,y] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in R ) ) ) ) & ( for x, y being Element of A holds
( [x,y] in b2 iff ( [x,y] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in R ) ) ) ) holds
b1 = b2
proof
defpred S1[ set , set ] means ( [$1,$2] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*$1*>) ^ q in dom f & (p ^ <*$2*>) ^ q in dom f holds
[(f . ((p ^ <*$1*>) ^ q)),(f . ((p ^ <*$2*>) ^ q))] in R ) );
thus for D1, D2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in D1 iff S1[x,y] ) ) & ( for x, y being Element of A holds
( [x,y] in D2 iff S1[x,y] ) ) holds
D1 = D2 from PUA2MSS1:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def5 defines |^ PUA2MSS1:def_5_:_
for A being partial non-empty UAStr
for R, b3 being Relation of the carrier of A holds
( b3 = R |^ A iff for x, y being Element of A holds
( [x,y] in b3 iff ( [x,y] in R & ( for f being operation of A
for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in R ) ) ) );
definition
let A be partial non-empty UAStr ;
let R be Relation of the carrier of A;
let i be Element of NAT ;
funcR |^ (A,i) -> Relation of the carrier of A means :Def6: :: PUA2MSS1:def 6
ex F being ManySortedSet of NAT st
( it = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) );
existence
ex b1 being Relation of the carrier of A ex F being ManySortedSet of NAT st
( b1 = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) )
proof
deffunc H1( Relation of the carrier of A, the carrier of A, Element of NAT ) -> Relation of the carrier of A = $1 |^ A;
thus ex D being Relation of the carrier of A ex F being ManySortedSet of NAT st
( D = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = H1(R,i) ) ) from PUA2MSS1:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of the carrier of A st ex F being ManySortedSet of NAT st
( b1 = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) ) & ex F being ManySortedSet of NAT st
( b2 = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) ) holds
b1 = b2
proof
deffunc H1( Relation of the carrier of A, the carrier of A, Element of NAT ) -> Relation of the carrier of A = $1 |^ A;
thus for D1, D2 being Relation of the carrier of A st ex F being ManySortedSet of NAT st
( D1 = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = H1(R,i) ) ) & ex F being ManySortedSet of NAT st
( D2 = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = H1(R,i) ) ) holds
D1 = D2 from PUA2MSS1:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def6 defines |^ PUA2MSS1:def_6_:_
for A being partial non-empty UAStr
for R being Relation of the carrier of A
for i being Element of NAT
for b4 being Relation of the carrier of A holds
( b4 = R |^ (A,i) iff ex F being ManySortedSet of NAT st
( b4 = F . i & F . 0 = R & ( for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) ) );
theorem Th16: :: PUA2MSS1:16
for A being partial non-empty UAStr
for R being Relation of the carrier of A holds
( R |^ (A,0) = R & R |^ (A,1) = R |^ A )
proof
let A be partial non-empty UAStr ; ::_thesis: for R being Relation of the carrier of A holds
( R |^ (A,0) = R & R |^ (A,1) = R |^ A )
let R be Relation of the carrier of A; ::_thesis: ( R |^ (A,0) = R & R |^ (A,1) = R |^ A )
consider F being ManySortedSet of NAT such that
R |^ (A,0) = F . 0 and
A1: F . 0 = R and
A2: for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A by Def6;
F . (0 + 1) = R |^ A by A1, A2;
hence ( R |^ (A,0) = R & R |^ (A,1) = R |^ A ) by A1, A2, Def6; ::_thesis: verum
end;
theorem Th17: :: PUA2MSS1:17
for A being partial non-empty UAStr
for i being Element of NAT
for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
proof
let A be partial non-empty UAStr ; ::_thesis: for i being Element of NAT
for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
let i be Element of NAT ; ::_thesis: for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
let R be Relation of the carrier of A; ::_thesis: R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
consider F being ManySortedSet of NAT such that
A1: R |^ (A,i) = F . i and
A2: F . 0 = R and
A3: for i being Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A by Def6;
F . (i + 1) = (R |^ (A,i)) |^ A by A1, A3;
hence R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A by A2, A3, Def6; ::_thesis: verum
end;
theorem :: PUA2MSS1:18
for A being partial non-empty UAStr
for i, j being Element of NAT
for R being Relation of the carrier of A holds R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j)
proof
let A be partial non-empty UAStr ; ::_thesis: for i, j being Element of NAT
for R being Relation of the carrier of A holds R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j)
let i, j be Element of NAT ; ::_thesis: for R being Relation of the carrier of A holds R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j)
let R be Relation of the carrier of A; ::_thesis: R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j)
defpred S1[ Element of NAT ] means R |^ (A,(i + $1)) = (R |^ (A,i)) |^ (A,$1);
A1: S1[ 0 ] by Th16;
A2: now__::_thesis:_for_j_being_Element_of_NAT_st_S1[j]_holds_
S1[j_+_1]
let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A3: S1[j] ; ::_thesis: S1[j + 1]
R |^ (A,(i + (j + 1))) = R |^ (A,((i + j) + 1))
.= (R |^ (A,(i + j))) |^ A by Th17
.= (R |^ (A,i)) |^ (A,(j + 1)) by A3, Th17 ;
hence S1[j + 1] ; ::_thesis: verum
end;
for j being Element of NAT holds S1[j] from NAT_1:sch_1(A1, A2);
hence R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j) ; ::_thesis: verum
end;
theorem Th19: :: PUA2MSS1:19
for A being partial non-empty UAStr
for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
( R |^ A is total & R |^ A is symmetric & R |^ A is transitive )
proof
let A be partial non-empty UAStr ; ::_thesis: for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
( R |^ A is total & R |^ A is symmetric & R |^ A is transitive )
let R be Equivalence_Relation of the carrier of A; ::_thesis: ( R c= DomRel A implies ( R |^ A is total & R |^ A is symmetric & R |^ A is transitive ) )
assume A1: R c= DomRel A ; ::_thesis: ( R |^ A is total & R |^ A is symmetric & R |^ A is transitive )
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_A_holds_
[x,x]_in_R_|^_A
let x be set ; ::_thesis: ( x in the carrier of A implies [x,x] in R |^ A )
assume x in the carrier of A ; ::_thesis: [x,x] in R |^ A
then reconsider a = x as Element of A ;
A2: [a,a] in R by EQREL_1:5;
now__::_thesis:_for_f_being_operation_of_A
for_p,_q_being_FinSequence_st_(p_^_<*a*>)_^_q_in_dom_f_&_(p_^_<*a*>)_^_q_in_dom_f_holds_
[(f_._((p_^_<*a*>)_^_q)),(f_._((p_^_<*a*>)_^_q))]_in_R
let f be operation of A; ::_thesis: for p, q being FinSequence st (p ^ <*a*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
let p, q be FinSequence; ::_thesis: ( (p ^ <*a*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R )
assume that
A3: (p ^ <*a*>) ^ q in dom f and
(p ^ <*a*>) ^ q in dom f ; ::_thesis: [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
f . ((p ^ <*a*>) ^ q) in rng f by A3, FUNCT_1:def_3;
hence [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R by EQREL_1:5; ::_thesis: verum
end;
hence [x,x] in R |^ A by A2, Def5; ::_thesis: verum
end;
then A4: R |^ A is_reflexive_in the carrier of A by RELAT_2:def_1;
then A5: dom (R |^ A) = the carrier of A by ORDERS_1:13;
A6: field (R |^ A) = the carrier of A by A4, ORDERS_1:13;
thus R |^ A is total by A5, PARTFUN1:def_2; ::_thesis: ( R |^ A is symmetric & R |^ A is transitive )
now__::_thesis:_for_x,_y_being_set_st_x_in_the_carrier_of_A_&_y_in_the_carrier_of_A_&_[x,y]_in_R_|^_A_holds_
[y,x]_in_R_|^_A
let x, y be set ; ::_thesis: ( x in the carrier of A & y in the carrier of A & [x,y] in R |^ A implies [y,x] in R |^ A )
assume that
A7: x in the carrier of A and
A8: y in the carrier of A ; ::_thesis: ( [x,y] in R |^ A implies [y,x] in R |^ A )
reconsider a = x, b = y as Element of A by A7, A8;
assume A9: [x,y] in R |^ A ; ::_thesis: [y,x] in R |^ A
then A10: [a,b] in R by Def5;
now__::_thesis:_(_[b,a]_in_R_&_(_for_f_being_operation_of_A
for_p,_q_being_FinSequence_st_(p_^_<*b*>)_^_q_in_dom_f_&_(p_^_<*a*>)_^_q_in_dom_f_holds_
[(f_._((p_^_<*b*>)_^_q)),(f_._((p_^_<*a*>)_^_q))]_in_R_)_)
thus [b,a] in R by A10, EQREL_1:6; ::_thesis: for f being operation of A
for p, q being FinSequence st (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
let f be operation of A; ::_thesis: for p, q being FinSequence st (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f holds
[(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
let p, q be FinSequence; ::_thesis: ( (p ^ <*b*>) ^ q in dom f & (p ^ <*a*>) ^ q in dom f implies [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R )
assume that
A11: (p ^ <*b*>) ^ q in dom f and
A12: (p ^ <*a*>) ^ q in dom f ; ::_thesis: [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*b*>) ^ q))] in R by A9, A11, A12, Def5;
hence [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*a*>) ^ q))] in R by EQREL_1:6; ::_thesis: verum
end;
hence [y,x] in R |^ A by Def5; ::_thesis: verum
end;
then R |^ A is_symmetric_in the carrier of A by RELAT_2:def_3;
hence R |^ A is symmetric by A6, RELAT_2:def_11; ::_thesis: R |^ A is transitive
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_the_carrier_of_A_&_y_in_the_carrier_of_A_&_z_in_the_carrier_of_A_&_[x,y]_in_R_|^_A_&_[y,z]_in_R_|^_A_holds_
[x,z]_in_R_|^_A
let x, y, z be set ; ::_thesis: ( x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in R |^ A & [y,z] in R |^ A implies [x,z] in R |^ A )
assume that
A13: x in the carrier of A and
A14: y in the carrier of A and
A15: z in the carrier of A ; ::_thesis: ( [x,y] in R |^ A & [y,z] in R |^ A implies [x,z] in R |^ A )
reconsider a = x, b = y, c = z as Element of A by A13, A14, A15;
assume that
A16: [x,y] in R |^ A and
A17: [y,z] in R |^ A ; ::_thesis: [x,z] in R |^ A
A18: now__::_thesis:_for_f_being_operation_of_A
for_p,_q_being_FinSequence_st_(p_^_<*a*>)_^_q_in_dom_f_&_(p_^_<*c*>)_^_q_in_dom_f_holds_
[(f_._((p_^_<*a*>)_^_q)),(f_._((p_^_<*c*>)_^_q))]_in_R
let f be operation of A; ::_thesis: for p, q being FinSequence st (p ^ <*a*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f holds
[(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R
let p, q be FinSequence; ::_thesis: ( (p ^ <*a*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R )
A19: [a,b] in R by A16, Def5;
A20: ( (p ^ <*a*>) ^ q in dom f & (p ^ <*b*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*b*>) ^ q))] in R ) by A16, Def5;
( (p ^ <*b*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f implies [(f . ((p ^ <*b*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R ) by A17, Def5;
hence ( (p ^ <*a*>) ^ q in dom f & (p ^ <*c*>) ^ q in dom f implies [(f . ((p ^ <*a*>) ^ q)),(f . ((p ^ <*c*>) ^ q))] in R ) by A1, A19, A20, Def4, EQREL_1:7; ::_thesis: verum
end;
A21: [a,b] in R by A16, Def5;
[b,c] in R by A17, Def5;
then [a,c] in R by A21, EQREL_1:7;
hence [x,z] in R |^ A by A18, Def5; ::_thesis: verum
end;
then R |^ A is_transitive_in the carrier of A by RELAT_2:def_8;
hence R |^ A is transitive by A6, RELAT_2:def_16; ::_thesis: verum
end;
theorem Th20: :: PUA2MSS1:20
for A being partial non-empty UAStr
for R being Relation of the carrier of A holds R |^ A c= R
proof
let A be partial non-empty UAStr ; ::_thesis: for R being Relation of the carrier of A holds R |^ A c= R
let R be Relation of the carrier of A; ::_thesis: R |^ A c= R
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in R |^ A or [x,y] in R )
assume A1: [x,y] in R |^ A ; ::_thesis: [x,y] in R
then A2: x in the carrier of A by ZFMISC_1:87;
y in the carrier of A by A1, ZFMISC_1:87;
hence [x,y] in R by A1, A2, Def5; ::_thesis: verum
end;
theorem Th21: :: PUA2MSS1:21
for A being partial non-empty UAStr
for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )
proof
let A be partial non-empty UAStr ; ::_thesis: for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )
let R be Equivalence_Relation of the carrier of A; ::_thesis: ( R c= DomRel A implies for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive ) )
assume A1: R c= DomRel A ; ::_thesis: for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )
defpred S1[ Element of NAT ] means ( R |^ (A,$1) c= DomRel A & R |^ (A,$1) is total & R |^ (A,$1) is symmetric & R |^ (A,$1) is transitive );
A2: S1[ 0 ] by A1, Th16;
A3: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; ::_thesis: S1[i + 1]
A5: (R |^ (A,i)) |^ A c= R |^ (A,i) by Th20;
(R |^ (A,i)) |^ A = R |^ (A,(i + 1)) by Th17;
hence S1[i + 1] by A4, A5, Th19, XBOOLE_1:1; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A2, A3);
hence for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive ) ; ::_thesis: verum
end;
definition
let A be partial non-empty UAStr ;
defpred S1[ set , set ] means for i being Element of NAT holds [$1,$2] in (DomRel A) |^ (A,i);
func LimDomRel A -> Relation of the carrier of A means :Def7: :: PUA2MSS1:def 7
for x, y being Element of A holds
( [x,y] in it iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) );
existence
ex b1 being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in b1 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) )
proof
thus ex D being Relation of the carrier of A st
for x, y being Element of A holds
( [x,y] in D iff S1[x,y] ) from RELSET_1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in b1 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) ) & ( for x, y being Element of A holds
( [x,y] in b2 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) ) holds
b1 = b2
proof
thus for D1, D2 being Relation of the carrier of A st ( for x, y being Element of A holds
( [x,y] in D1 iff S1[x,y] ) ) & ( for x, y being Element of A holds
( [x,y] in D2 iff S1[x,y] ) ) holds
D1 = D2 from PUA2MSS1:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def7 defines LimDomRel PUA2MSS1:def_7_:_
for A being partial non-empty UAStr
for b2 being Relation of the carrier of A holds
( b2 = LimDomRel A iff for x, y being Element of A holds
( [x,y] in b2 iff for i being Element of NAT holds [x,y] in (DomRel A) |^ (A,i) ) );
theorem Th22: :: PUA2MSS1:22
for A being partial non-empty UAStr holds LimDomRel A c= DomRel A
proof
let A be partial non-empty UAStr ; ::_thesis: LimDomRel A c= DomRel A
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in LimDomRel A or [x,y] in DomRel A )
assume A1: [x,y] in LimDomRel A ; ::_thesis: [x,y] in DomRel A
then A2: x in the carrier of A by ZFMISC_1:87;
y in the carrier of A by A1, ZFMISC_1:87;
then [x,y] in (DomRel A) |^ (A,0) by A1, A2, Def7;
hence [x,y] in DomRel A by Th16; ::_thesis: verum
end;
registration
let A be partial non-empty UAStr ;
cluster LimDomRel A -> total symmetric transitive ;
coherence
( LimDomRel A is total & LimDomRel A is symmetric & LimDomRel A is transitive )
proof
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_A_holds_
[x,x]_in_LimDomRel_A
let x be set ; ::_thesis: ( x in the carrier of A implies [x,x] in LimDomRel A )
assume x in the carrier of A ; ::_thesis: [x,x] in LimDomRel A
then reconsider a = x as Element of A ;
now__::_thesis:_for_i_being_Element_of_NAT_holds_[a,a]_in_(DomRel_A)_|^_(A,i)
let i be Element of NAT ; ::_thesis: [a,a] in (DomRel A) |^ (A,i)
( (DomRel A) |^ (A,i) is total & (DomRel A) |^ (A,i) is symmetric & (DomRel A) |^ (A,i) is transitive ) by Th21;
hence [a,a] in (DomRel A) |^ (A,i) by EQREL_1:5; ::_thesis: verum
end;
hence [x,x] in LimDomRel A by Def7; ::_thesis: verum
end;
then A1: LimDomRel A is_reflexive_in the carrier of A by RELAT_2:def_1;
then A2: dom (LimDomRel A) = the carrier of A by ORDERS_1:13;
A3: field (LimDomRel A) = the carrier of A by A1, ORDERS_1:13;
thus LimDomRel A is total by A2, PARTFUN1:def_2; ::_thesis: ( LimDomRel A is symmetric & LimDomRel A is transitive )
now__::_thesis:_for_x,_y_being_set_st_x_in_the_carrier_of_A_&_y_in_the_carrier_of_A_&_[x,y]_in_LimDomRel_A_holds_
[y,x]_in_LimDomRel_A
let x, y be set ; ::_thesis: ( x in the carrier of A & y in the carrier of A & [x,y] in LimDomRel A implies [y,x] in LimDomRel A )
assume that
A4: x in the carrier of A and
A5: y in the carrier of A ; ::_thesis: ( [x,y] in LimDomRel A implies [y,x] in LimDomRel A )
reconsider a = x, b = y as Element of A by A4, A5;
assume A6: [x,y] in LimDomRel A ; ::_thesis: [y,x] in LimDomRel A
now__::_thesis:_for_i_being_Element_of_NAT_holds_[b,a]_in_(DomRel_A)_|^_(A,i)
let i be Element of NAT ; ::_thesis: [b,a] in (DomRel A) |^ (A,i)
A7: ( (DomRel A) |^ (A,i) is total & (DomRel A) |^ (A,i) is symmetric & (DomRel A) |^ (A,i) is transitive ) by Th21;
[a,b] in (DomRel A) |^ (A,i) by A6, Def7;
hence [b,a] in (DomRel A) |^ (A,i) by A7, EQREL_1:6; ::_thesis: verum
end;
hence [y,x] in LimDomRel A by Def7; ::_thesis: verum
end;
then LimDomRel A is_symmetric_in the carrier of A by RELAT_2:def_3;
hence LimDomRel A is symmetric by A3, RELAT_2:def_11; ::_thesis: LimDomRel A is transitive
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_the_carrier_of_A_&_y_in_the_carrier_of_A_&_z_in_the_carrier_of_A_&_[x,y]_in_LimDomRel_A_&_[y,z]_in_LimDomRel_A_holds_
[x,z]_in_LimDomRel_A
let x, y, z be set ; ::_thesis: ( x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in LimDomRel A & [y,z] in LimDomRel A implies [x,z] in LimDomRel A )
assume that
A8: x in the carrier of A and
A9: y in the carrier of A and
A10: z in the carrier of A ; ::_thesis: ( [x,y] in LimDomRel A & [y,z] in LimDomRel A implies [x,z] in LimDomRel A )
reconsider a = x, b = y, c = z as Element of A by A8, A9, A10;
assume that
A11: [x,y] in LimDomRel A and
A12: [y,z] in LimDomRel A ; ::_thesis: [x,z] in LimDomRel A
now__::_thesis:_for_i_being_Element_of_NAT_holds_[a,c]_in_(DomRel_A)_|^_(A,i)
let i be Element of NAT ; ::_thesis: [a,c] in (DomRel A) |^ (A,i)
A13: ( (DomRel A) |^ (A,i) is total & (DomRel A) |^ (A,i) is symmetric & (DomRel A) |^ (A,i) is transitive ) by Th21;
A14: [a,b] in (DomRel A) |^ (A,i) by A11, Def7;
[b,c] in (DomRel A) |^ (A,i) by A12, Def7;
hence [a,c] in (DomRel A) |^ (A,i) by A13, A14, EQREL_1:7; ::_thesis: verum
end;
hence [x,z] in LimDomRel A by Def7; ::_thesis: verum
end;
then LimDomRel A is_transitive_in the carrier of A by RELAT_2:def_8;
hence LimDomRel A is transitive by A3, RELAT_2:def_16; ::_thesis: verum
end;
end;
begin
definition
let X be non empty set ;
let f be PartFunc of (X *),X;
let P be a_partition of X;
predf is_partitable_wrt P means :Def8: :: PUA2MSS1:def 8
for p being FinSequence of P ex a being Element of P st f .: (product p) c= a;
end;
:: deftheorem Def8 defines is_partitable_wrt PUA2MSS1:def_8_:_
for X being non empty set
for f being PartFunc of (X *),X
for P being a_partition of X holds
( f is_partitable_wrt P iff for p being FinSequence of P ex a being Element of P st f .: (product p) c= a );
definition
let X be non empty set ;
let f be PartFunc of (X *),X;
let P be a_partition of X;
predf is_exactly_partitable_wrt P means :Def9: :: PUA2MSS1:def 9
( f is_partitable_wrt P & ( for p being FinSequence of P st product p meets dom f holds
product p c= dom f ) );
end;
:: deftheorem Def9 defines is_exactly_partitable_wrt PUA2MSS1:def_9_:_
for X being non empty set
for f being PartFunc of (X *),X
for P being a_partition of X holds
( f is_exactly_partitable_wrt P iff ( f is_partitable_wrt P & ( for p being FinSequence of P st product p meets dom f holds
product p c= dom f ) ) );
theorem :: PUA2MSS1:23
for A being partial non-empty UAStr
for f being operation of A holds f is_exactly_partitable_wrt SmallestPartition the carrier of A
proof
let A be partial non-empty UAStr ; ::_thesis: for f being operation of A holds f is_exactly_partitable_wrt SmallestPartition the carrier of A
set P = SmallestPartition the carrier of A;
let f be operation of A; ::_thesis: f is_exactly_partitable_wrt SmallestPartition the carrier of A
hereby :: according to PUA2MSS1:def_8,PUA2MSS1:def_9 ::_thesis: for p being FinSequence of SmallestPartition the carrier of A st product p meets dom f holds
product p c= dom f
let p be FinSequence of SmallestPartition the carrier of A; ::_thesis: ex a being Element of SmallestPartition the carrier of A st f .: (product p) c= a
consider q being FinSequence of the carrier of A such that
A1: product p = {q} by Th13;
( ( q in dom f & f . q in rng f & rng f c= the carrier of A ) or not q in dom f ) by FUNCT_1:def_3;
then consider x being Element of A such that
A2: ( ( q in dom f & x = f . q ) or not q in dom f ) ;
SmallestPartition the carrier of A = { {z} where z is Element of A : verum } by EQREL_1:37;
then {x} in SmallestPartition the carrier of A ;
then reconsider a = {x} as Element of SmallestPartition the carrier of A ;
take a = a; ::_thesis: f .: (product p) c= a
thus f .: (product p) c= a ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in f .: (product p) or z in a )
assume z in f .: (product p) ; ::_thesis: z in a
then consider y being set such that
A3: y in dom f and
A4: y in product p and
A5: z = f . y by FUNCT_1:def_6;
y = q by A1, A4, TARSKI:def_1;
hence z in a by A2, A3, A5, TARSKI:def_1; ::_thesis: verum
end;
end;
let p be FinSequence of SmallestPartition the carrier of A; ::_thesis: ( product p meets dom f implies product p c= dom f )
consider q being FinSequence of the carrier of A such that
A6: product p = {q} by Th13;
assume product p meets dom f ; ::_thesis: product p c= dom f
then A7: ex x being set st
( x in product p & x in dom f ) by XBOOLE_0:3;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in product p or z in dom f )
assume z in product p ; ::_thesis: z in dom f
then z = q by A6, TARSKI:def_1;
hence z in dom f by A6, A7, TARSKI:def_1; ::_thesis: verum
end;
scheme :: PUA2MSS1:sch 4
FiniteTransitivity{ F1() -> FinSequence, F2() -> FinSequence, P1[ set ], P2[ set , set ] } :
P1[F2()]
provided
A1: P1[F1()] and
A2: len F1() = len F2() and
A3: for p, q being FinSequence
for z1, z2 being set st P1[(p ^ <*z1*>) ^ q] & P2[z1,z2] holds
P1[(p ^ <*z2*>) ^ q] and
A4: for i being Element of NAT st i in dom F1() holds
P2[F1() . i,F2() . i]
proof
defpred S1[ Element of NAT ] means for x1, x2, y1, y2 being FinSequence st len x1 = $1 & F1() = x1 ^ x2 & len y1 = $1 & F2() = y1 ^ y2 holds
P1[y1 ^ x2];
A5: S1[ 0 ]
proof
let x1, x2, y1, y2 be FinSequence; ::_thesis: ( len x1 = 0 & F1() = x1 ^ x2 & len y1 = 0 & F2() = y1 ^ y2 implies P1[y1 ^ x2] )
assume that
A6: len x1 = 0 and
A7: F1() = x1 ^ x2 and
A8: len y1 = 0 and
F2() = y1 ^ y2 ; ::_thesis: P1[y1 ^ x2]
A9: x1 = {} by A6;
y1 = {} by A8;
hence P1[y1 ^ x2] by A1, A7, A9; ::_thesis: verum
end;
A10: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A11: for x1, x2, y1, y2 being FinSequence st len x1 = i & F1() = x1 ^ x2 & len y1 = i & F2() = y1 ^ y2 holds
P1[y1 ^ x2] ; ::_thesis: S1[i + 1]
let x1, x2, y1, y2 be FinSequence; ::_thesis: ( len x1 = i + 1 & F1() = x1 ^ x2 & len y1 = i + 1 & F2() = y1 ^ y2 implies P1[y1 ^ x2] )
assume that
A12: len x1 = i + 1 and
A13: F1() = x1 ^ x2 and
A14: len y1 = i + 1 and
A15: F2() = y1 ^ y2 ; ::_thesis: P1[y1 ^ x2]
A16: x1 <> {} by A12;
A17: y1 <> {} by A14;
consider x9 being FinSequence, xx being set such that
A18: x1 = x9 ^ <*xx*> by A16, FINSEQ_1:46;
consider y9 being FinSequence, yy being set such that
A19: y1 = y9 ^ <*yy*> by A17, FINSEQ_1:46;
A20: dom x1 = Seg (len x1) by FINSEQ_1:def_3;
A21: dom y1 = Seg (len y1) by FINSEQ_1:def_3;
A22: len <*xx*> = 1 by FINSEQ_1:40;
A23: len <*yy*> = 1 by FINSEQ_1:40;
A24: len x1 = (len x9) + 1 by A18, A22, FINSEQ_1:22;
A25: len y1 = (len y9) + 1 by A19, A23, FINSEQ_1:22;
A26: F1() = x9 ^ (<*xx*> ^ x2) by A13, A18, FINSEQ_1:32;
A27: F2() = y9 ^ (<*yy*> ^ y2) by A15, A19, FINSEQ_1:32;
A28: i + 1 in dom x1 by A12, A20, FINSEQ_1:4;
A29: dom x1 c= dom F1() by A13, FINSEQ_1:26;
A30: x1 . ((len x9) + 1) = xx by A18, FINSEQ_1:42;
A31: y1 . ((len y9) + 1) = yy by A19, FINSEQ_1:42;
A32: P1[y9 ^ (<*xx*> ^ x2)] by A11, A12, A14, A24, A25, A26, A27;
A33: F1() . (i + 1) = xx by A12, A13, A24, A28, A30, FINSEQ_1:def_7;
A34: F2() . (i + 1) = yy by A12, A14, A15, A20, A21, A25, A28, A31, FINSEQ_1:def_7;
P1[(y9 ^ <*xx*>) ^ x2] by A32, FINSEQ_1:32;
hence P1[y1 ^ x2] by A3, A4, A19, A28, A29, A33, A34; ::_thesis: verum
end;
A35: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A5, A10);
A36: F1() = F1() ^ {} by FINSEQ_1:34;
F2() = F2() ^ {} by FINSEQ_1:34;
hence P1[F2()] by A2, A35, A36; ::_thesis: verum
end;
theorem Th24: :: PUA2MSS1:24
for A being partial non-empty UAStr
for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A)
proof
let A be partial non-empty UAStr ; ::_thesis: for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A)
set P = Class (LimDomRel A);
let f be operation of A; ::_thesis: f is_exactly_partitable_wrt Class (LimDomRel A)
hereby :: according to PUA2MSS1:def_8,PUA2MSS1:def_9 ::_thesis: for p being FinSequence of Class (LimDomRel A) st product p meets dom f holds
product p c= dom f
let p be FinSequence of Class (LimDomRel A); ::_thesis: ex a being Element of Class (LimDomRel A) st f .: (product a) c= b2
set a0 = the Element of Class (LimDomRel A);
percases ( product p meets dom f or product p misses dom f ) ;
suppose product p meets dom f ; ::_thesis: ex a being Element of Class (LimDomRel A) st f .: (product a) c= b2
then consider x being set such that
A1: x in product p and
A2: x in dom f by XBOOLE_0:3;
f . x in the carrier of A by A2, PARTFUN1:4;
then reconsider a = Class ((LimDomRel A),(f . x)) as Element of Class (LimDomRel A) by EQREL_1:def_3;
take a = a; ::_thesis: f .: (product p) c= a
thus f .: (product p) c= a ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (product p) or y in a )
assume y in f .: (product p) ; ::_thesis: y in a
then consider z being set such that
z in dom f and
A3: z in product p and
A4: y = f . z by FUNCT_1:def_6;
A5: product p c= Funcs ((dom p),(Union p)) by FUNCT_6:1;
then A6: ex f being Function st
( x = f & dom f = dom p & rng f c= Union p ) by A1, FUNCT_2:def_2;
A7: ex f being Function st
( z = f & dom f = dom p & rng f c= Union p ) by A3, A5, FUNCT_2:def_2;
reconsider x = x, z = z as Function by A1, A3;
A8: dom p = Seg (len p) by FINSEQ_1:def_3;
then reconsider x = x, z = z as FinSequence by A6, A7, FINSEQ_1:def_2;
defpred S1[ set ] means ( $1 in dom f & f . $1 in a );
defpred S2[ set , set ] means [$1,$2] in LimDomRel A;
len x = len p by A6, A8, FINSEQ_1:def_3;
then A9: len x = len z by A7, A8, FINSEQ_1:def_3;
A10: S1[x] by A2, EQREL_1:20, PARTFUN1:4;
A11: for p1, q1 being FinSequence
for z1, z2 being set st S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] holds
S1[(p1 ^ <*z2*>) ^ q1]
proof
let p1, q1 be FinSequence; ::_thesis: for z1, z2 being set st S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] holds
S1[(p1 ^ <*z2*>) ^ q1]
let z1, z2 be set ; ::_thesis: ( S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] implies S1[(p1 ^ <*z2*>) ^ q1] )
assume that
A12: (p1 ^ <*z1*>) ^ q1 in dom f and
A13: f . ((p1 ^ <*z1*>) ^ q1) in a and
A14: [z1,z2] in LimDomRel A ; ::_thesis: S1[(p1 ^ <*z2*>) ^ q1]
A15: [(f . ((p1 ^ <*z1*>) ^ q1)),(f . x)] in LimDomRel A by A13, EQREL_1:19;
A16: LimDomRel A c= DomRel A by Th22;
A17: z1 in the carrier of A by A14, ZFMISC_1:87;
A18: z2 in the carrier of A by A14, ZFMISC_1:87;
hence A19: (p1 ^ <*z2*>) ^ q1 in dom f by A12, A14, A16, A17, Def4; ::_thesis: f . ((p1 ^ <*z2*>) ^ q1) in a
A20: f . ((p1 ^ <*z1*>) ^ q1) in rng f by A12, FUNCT_1:def_3;
A21: f . ((p1 ^ <*z2*>) ^ q1) in rng f by A19, FUNCT_1:def_3;
now__::_thesis:_for_i_being_Element_of_NAT_holds_[(f_._((p1_^_<*z2*>)_^_q1)),(f_._((p1_^_<*z1*>)_^_q1))]_in_(DomRel_A)_|^_(A,i)
let i be Element of NAT ; ::_thesis: [(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in (DomRel A) |^ (A,i)
[z1,z2] in (DomRel A) |^ (A,(i + 1)) by A14, A17, A18, Def7;
then [z1,z2] in ((DomRel A) |^ (A,i)) |^ A by Th17;
then A22: [(f . ((p1 ^ <*z1*>) ^ q1)),(f . ((p1 ^ <*z2*>) ^ q1))] in (DomRel A) |^ (A,i) by A12, A17, A18, A19, Def5;
( (DomRel A) |^ (A,i) is total & (DomRel A) |^ (A,i) is symmetric & (DomRel A) |^ (A,i) is transitive ) by Th21;
hence [(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in (DomRel A) |^ (A,i) by A22, EQREL_1:6; ::_thesis: verum
end;
then [(f . ((p1 ^ <*z2*>) ^ q1)),(f . ((p1 ^ <*z1*>) ^ q1))] in LimDomRel A by A20, A21, Def7;
then [(f . ((p1 ^ <*z2*>) ^ q1)),(f . x)] in LimDomRel A by A15, EQREL_1:7;
hence f . ((p1 ^ <*z2*>) ^ q1) in a by EQREL_1:19; ::_thesis: verum
end;
A23: for i being Element of NAT st i in dom x holds
S2[x . i,z . i]
proof
let i be Element of NAT ; ::_thesis: ( i in dom x implies S2[x . i,z . i] )
assume A24: i in dom x ; ::_thesis: S2[x . i,z . i]
then p . i in rng p by A6, FUNCT_1:def_3;
then reconsider a = p . i as Element of Class (LimDomRel A) ;
A25: ex g being Function st
( x = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) by A1, CARD_3:def_5;
A26: ex g being Function st
( z = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) by A3, CARD_3:def_5;
A27: ex b being set st
( b in the carrier of A & a = Class ((LimDomRel A),b) ) by EQREL_1:def_3;
A28: x . i in a by A24, A25;
z . i in a by A24, A25, A26;
hence S2[x . i,z . i] by A27, A28, EQREL_1:22; ::_thesis: verum
end;
S1[z] from PUA2MSS1:sch_4(A10, A9, A11, A23);
hence y in a by A4; ::_thesis: verum
end;
end;
suppose product p misses dom f ; ::_thesis: ex a being Element of Class (LimDomRel A) st f .: (product a) c= b2
then (product p) /\ (dom f) = {} by XBOOLE_0:def_7;
then f .: (product p) = f .: {} by RELAT_1:112
.= {} ;
then f .: (product p) c= the Element of Class (LimDomRel A) by XBOOLE_1:2;
hence ex a being Element of Class (LimDomRel A) st f .: (product p) c= a ; ::_thesis: verum
end;
end;
end;
let p be FinSequence of Class (LimDomRel A); ::_thesis: ( product p meets dom f implies product p c= dom f )
assume product p meets dom f ; ::_thesis: product p c= dom f
then consider x being set such that
A29: x in product p and
A30: x in dom f by XBOOLE_0:3;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in product p or y in dom f )
assume A31: y in product p ; ::_thesis: y in dom f
A32: product p c= Funcs ((dom p),(Union p)) by FUNCT_6:1;
then A33: ex f being Function st
( x = f & dom f = dom p & rng f c= Union p ) by A29, FUNCT_2:def_2;
A34: ex f being Function st
( y = f & dom f = dom p & rng f c= Union p ) by A31, A32, FUNCT_2:def_2;
reconsider x = x, z = y as Function by A29, A31;
A35: dom p = Seg (len p) by FINSEQ_1:def_3;
then reconsider x = x, z = z as FinSequence by A33, A34, FINSEQ_1:def_2;
defpred S1[ set ] means $1 in dom f;
defpred S2[ set , set ] means [$1,$2] in LimDomRel A;
len x = len p by A33, A35, FINSEQ_1:def_3;
then A36: len x = len z by A34, A35, FINSEQ_1:def_3;
A37: S1[x] by A30;
A38: for p1, q1 being FinSequence
for z1, z2 being set st S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] holds
S1[(p1 ^ <*z2*>) ^ q1]
proof
let p1, q1 be FinSequence; ::_thesis: for z1, z2 being set st S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] holds
S1[(p1 ^ <*z2*>) ^ q1]
let z1, z2 be set ; ::_thesis: ( S1[(p1 ^ <*z1*>) ^ q1] & S2[z1,z2] implies S1[(p1 ^ <*z2*>) ^ q1] )
assume that
A39: (p1 ^ <*z1*>) ^ q1 in dom f and
A40: [z1,z2] in LimDomRel A ; ::_thesis: S1[(p1 ^ <*z2*>) ^ q1]
A41: LimDomRel A c= DomRel A by Th22;
A42: z1 in the carrier of A by A40, ZFMISC_1:87;
z2 in the carrier of A by A40, ZFMISC_1:87;
hence S1[(p1 ^ <*z2*>) ^ q1] by A39, A40, A41, A42, Def4; ::_thesis: verum
end;
A43: for i being Element of NAT st i in dom x holds
S2[x . i,z . i]
proof
let i be Element of NAT ; ::_thesis: ( i in dom x implies S2[x . i,z . i] )
assume A44: i in dom x ; ::_thesis: S2[x . i,z . i]
then p . i in rng p by A33, FUNCT_1:def_3;
then reconsider a = p . i as Element of Class (LimDomRel A) ;
A45: ex g being Function st
( x = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) by A29, CARD_3:def_5;
A46: ex g being Function st
( z = g & dom g = dom p & ( for x being set st x in dom p holds
g . x in p . x ) ) by A31, CARD_3:def_5;
A47: ex b being set st
( b in the carrier of A & a = Class ((LimDomRel A),b) ) by EQREL_1:def_3;
A48: x . i in a by A44, A45;
z . i in a by A44, A45, A46;
hence S2[x . i,z . i] by A47, A48, EQREL_1:22; ::_thesis: verum
end;
S1[z] from PUA2MSS1:sch_4(A37, A36, A38, A43);
hence y in dom f ; ::_thesis: verum
end;
definition
let A be partial non-empty UAStr ;
mode a_partition of A -> a_partition of the carrier of A means :Def10: :: PUA2MSS1:def 10
for f being operation of A holds f is_exactly_partitable_wrt it;
existence
ex b1 being a_partition of the carrier of A st
for f being operation of A holds f is_exactly_partitable_wrt b1
proof
for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A) by Th24;
hence ex b1 being a_partition of the carrier of A st
for f being operation of A holds f is_exactly_partitable_wrt b1 ; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines a_partition PUA2MSS1:def_10_:_
for A being partial non-empty UAStr
for b2 being a_partition of the carrier of A holds
( b2 is a_partition of A iff for f being operation of A holds f is_exactly_partitable_wrt b2 );
definition
let A be partial non-empty UAStr ;
mode IndexedPartition of A -> IndexedPartition of the carrier of A means :Def11: :: PUA2MSS1:def 11
rng it is a_partition of A;
existence
ex b1 being IndexedPartition of the carrier of A st rng b1 is a_partition of A
proof
set P = the a_partition of A;
take id the a_partition of A ; ::_thesis: rng (id the a_partition of A) is a_partition of A
thus rng (id the a_partition of A) is a_partition of A ; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines IndexedPartition PUA2MSS1:def_11_:_
for A being partial non-empty UAStr
for b2 being IndexedPartition of the carrier of A holds
( b2 is IndexedPartition of A iff rng b2 is a_partition of A );
definition
let A be partial non-empty UAStr ;
let P be IndexedPartition of A;
:: original: proj2
redefine func rng P -> a_partition of A;
coherence
proj2 P is a_partition of A by Def11;
end;
theorem :: PUA2MSS1:25
for A being partial non-empty UAStr holds Class (LimDomRel A) is a_partition of A
proof
let A be partial non-empty UAStr ; ::_thesis: Class (LimDomRel A) is a_partition of A
thus for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A) by Th24; :: according to PUA2MSS1:def_10 ::_thesis: verum
end;
theorem Th26: :: PUA2MSS1:26
for X being non empty set
for P being a_partition of X
for p being FinSequence of P
for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product p & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product p
proof
let X be non empty set ; ::_thesis: for P being a_partition of X
for p being FinSequence of P
for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product p & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product p
let P be a_partition of X; ::_thesis: for p being FinSequence of P
for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product p & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product p
let pp be FinSequence of P; ::_thesis: for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product pp & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product pp
let p, q be FinSequence; ::_thesis: for x, y being set st (p ^ <*x*>) ^ q in product pp & ex a being Element of P st
( x in a & y in a ) holds
(p ^ <*y*>) ^ q in product pp
let x, y be set ; ::_thesis: ( (p ^ <*x*>) ^ q in product pp & ex a being Element of P st
( x in a & y in a ) implies (p ^ <*y*>) ^ q in product pp )
assume A1: (p ^ <*x*>) ^ q in product pp ; ::_thesis: ( for a being Element of P holds
( not x in a or not y in a ) or (p ^ <*y*>) ^ q in product pp )
given a being Element of P such that A2: x in a and
A3: y in a ; ::_thesis: (p ^ <*y*>) ^ q in product pp
reconsider x = x, y = y as Element of a by A2, A3;
now__::_thesis:_(_dom_((p_^_<*y*>)_^_q)_=_dom_pp_&_(_for_i_being_set_st_i_in_dom_pp_holds_
((p_^_<*y*>)_^_q)_._i_in_pp_._i_)_)
A4: ex g being Function st
( (p ^ <*x*>) ^ q = g & dom g = dom pp & ( for x being set st x in dom pp holds
g . x in pp . x ) ) by A1, CARD_3:def_5;
thus dom ((p ^ <*y*>) ^ q) = Seg (len ((p ^ <*y*>) ^ q)) by FINSEQ_1:def_3
.= Seg ((len (p ^ <*y*>)) + (len q)) by FINSEQ_1:22
.= Seg (((len p) + (len <*y*>)) + (len q)) by FINSEQ_1:22
.= Seg (((len p) + 1) + (len q)) by FINSEQ_1:40
.= Seg (((len p) + (len <*x*>)) + (len q)) by FINSEQ_1:40
.= Seg ((len (p ^ <*x*>)) + (len q)) by FINSEQ_1:22
.= Seg (len ((p ^ <*x*>) ^ q)) by FINSEQ_1:22
.= dom pp by A4, FINSEQ_1:def_3 ; ::_thesis: for i being set st i in dom pp holds
((p ^ <*y*>) ^ q) . b2 in pp . b2
let i be set ; ::_thesis: ( i in dom pp implies ((p ^ <*y*>) ^ q) . b1 in pp . b1 )
assume A5: i in dom pp ; ::_thesis: ((p ^ <*y*>) ^ q) . b1 in pp . b1
then reconsider ii = i as Element of NAT ;
A6: len <*x*> = 1 by FINSEQ_1:40;
A7: len <*y*> = 1 by FINSEQ_1:40;
A8: dom <*x*> = Seg 1 by FINSEQ_1:38;
A9: len (p ^ <*x*>) = (len p) + 1 by A6, FINSEQ_1:22;
A10: len (p ^ <*y*>) = (len p) + 1 by A7, FINSEQ_1:22;
A11: dom (p ^ <*x*>) = Seg ((len p) + 1) by A9, FINSEQ_1:def_3;
A12: dom (p ^ <*y*>) = Seg ((len p) + 1) by A10, FINSEQ_1:def_3;
A13: ( ii in dom (p ^ <*x*>) or ex n being Nat st
( n in dom q & ii = (len (p ^ <*x*>)) + n ) ) by A4, A5, FINSEQ_1:25;
A14: dom p c= dom (p ^ <*y*>) by FINSEQ_1:26;
percases ( ii in dom p or ex n being Nat st
( n in dom <*x*> & ii = (len p) + n ) or ex n being Element of NAT st
( n in dom q & ii = (len (p ^ <*x*>)) + n ) ) by A13, FINSEQ_1:25;
supposeA15: ii in dom p ; ::_thesis: ((p ^ <*y*>) ^ q) . b1 in pp . b1
then A16: (p ^ <*y*>) . i = p . i by FINSEQ_1:def_7;
A17: (p ^ <*x*>) . i = p . i by A15, FINSEQ_1:def_7;
A18: ((p ^ <*y*>) ^ q) . i = p . i by A14, A15, A16, FINSEQ_1:def_7;
((p ^ <*x*>) ^ q) . i = p . i by A11, A12, A14, A15, A17, FINSEQ_1:def_7;
hence ((p ^ <*y*>) ^ q) . i in pp . i by A4, A5, A18; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom <*x*> & ii = (len p) + n ) ; ::_thesis: ((p ^ <*y*>) ^ q) . b1 in pp . b1
then consider n being Nat such that
A19: n in Seg 1 and
A20: ii = (len p) + n by A8;
A21: n = 1 by A19, FINSEQ_1:2, TARSKI:def_1;
then A22: (p ^ <*x*>) . ii = x by A20, FINSEQ_1:42;
A23: (p ^ <*y*>) . ii = y by A20, A21, FINSEQ_1:42;
A24: ii in dom (p ^ <*y*>) by A12, A20, A21, FINSEQ_1:4;
then A25: ((p ^ <*x*>) ^ q) . ii = x by A11, A12, A22, FINSEQ_1:def_7;
A26: ((p ^ <*y*>) ^ q) . ii = y by A23, A24, FINSEQ_1:def_7;
A27: x in pp . i by A4, A5, A25;
pp . i in rng pp by A5, FUNCT_1:def_3;
then A28: pp . i in P ;
a meets pp . i by A27, XBOOLE_0:3;
then pp . i = a by A28, EQREL_1:def_4;
hence ((p ^ <*y*>) ^ q) . i in pp . i by A26; ::_thesis: verum
end;
suppose ex n being Element of NAT st
( n in dom q & ii = (len (p ^ <*x*>)) + n ) ; ::_thesis: ((p ^ <*y*>) ^ q) . b1 in pp . b1
then consider n being Element of NAT such that
A29: n in dom q and
A30: ii = (len (p ^ <*x*>)) + n ;
A31: ((p ^ <*y*>) ^ q) . i = q . n by A9, A10, A29, A30, FINSEQ_1:def_7;
((p ^ <*x*>) ^ q) . i = q . n by A29, A30, FINSEQ_1:def_7;
hence ((p ^ <*y*>) ^ q) . i in pp . i by A4, A5, A31; ::_thesis: verum
end;
end;
end;
hence (p ^ <*y*>) ^ q in product pp by CARD_3:def_5; ::_thesis: verum
end;
theorem Th27: :: PUA2MSS1:27
for A being partial non-empty UAStr
for P being a_partition of A holds P is_finer_than Class (LimDomRel A)
proof
let A be partial non-empty UAStr ; ::_thesis: for P being a_partition of A holds P is_finer_than Class (LimDomRel A)
let P be a_partition of A; ::_thesis: P is_finer_than Class (LimDomRel A)
consider EP being Equivalence_Relation of the carrier of A such that
A1: P = Class EP by EQREL_1:34;
let a be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not a in P or ex b1 being set st
( b1 in Class (LimDomRel A) & a c= b1 ) )
assume a in P ; ::_thesis: ex b1 being set st
( b1 in Class (LimDomRel A) & a c= b1 )
then reconsider aa = a as Element of P ;
set x = the Element of aa;
take Class ((LimDomRel A), the Element of aa) ; ::_thesis: ( Class ((LimDomRel A), the Element of aa) in Class (LimDomRel A) & a c= Class ((LimDomRel A), the Element of aa) )
thus Class ((LimDomRel A), the Element of aa) in Class (LimDomRel A) by EQREL_1:def_3; ::_thesis: a c= Class ((LimDomRel A), the Element of aa)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in Class ((LimDomRel A), the Element of aa) )
assume y in a ; ::_thesis: y in Class ((LimDomRel A), the Element of aa)
then reconsider y = y as Element of aa ;
reconsider x = the Element of aa, y = y as Element of A ;
defpred S1[ Element of NAT ] means EP c= (DomRel A) |^ (A,$1);
A2: S1[ 0 ]
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in EP or [x,y] in (DomRel A) |^ (A,0) )
assume A3: [x,y] in EP ; ::_thesis: [x,y] in (DomRel A) |^ (A,0)
then reconsider x = x, y = y as Element of A by ZFMISC_1:87;
reconsider a = Class (EP,y) as Element of P by A1, EQREL_1:def_3;
A4: x in a by A3, EQREL_1:19;
A5: y in a by EQREL_1:20;
for f being operation of A
for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )
proof
let f be operation of A; ::_thesis: for p, q being FinSequence holds
( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )
let p, q be FinSequence; ::_thesis: ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f )
A6: f is_exactly_partitable_wrt P by Def10;
now__::_thesis:_for_p,_q_being_FinSequence
for_x,_y_being_Element_of_a_st_(p_^_<*x*>)_^_q_in_dom_f_holds_
(p_^_<*y*>)_^_q_in_dom_f
let p, q be FinSequence; ::_thesis: for x, y being Element of a st (p ^ <*x*>) ^ q in dom f holds
(p ^ <*y*>) ^ q in dom f
let x, y be Element of a; ::_thesis: ( (p ^ <*x*>) ^ q in dom f implies (p ^ <*y*>) ^ q in dom f )
assume A7: (p ^ <*x*>) ^ q in dom f ; ::_thesis: (p ^ <*y*>) ^ q in dom f
then (p ^ <*x*>) ^ q is FinSequence of the carrier of A by FINSEQ_1:def_11;
then consider pp being FinSequence of P such that
A8: (p ^ <*x*>) ^ q in product pp by Th7;
product pp meets dom f by A7, A8, XBOOLE_0:3;
then A9: product pp c= dom f by A6, Def9;
(p ^ <*y*>) ^ q in product pp by A8, Th26;
hence (p ^ <*y*>) ^ q in dom f by A9; ::_thesis: verum
end;
hence ( (p ^ <*x*>) ^ q in dom f iff (p ^ <*y*>) ^ q in dom f ) by A4, A5; ::_thesis: verum
end;
then [x,y] in DomRel A by Def4;
hence [x,y] in (DomRel A) |^ (A,0) by Th16; ::_thesis: verum
end;
A10: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A11: EP c= (DomRel A) |^ (A,i) ; ::_thesis: S1[i + 1]
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in EP or [x,y] in (DomRel A) |^ (A,(i + 1)) )
assume A12: [x,y] in EP ; ::_thesis: [x,y] in (DomRel A) |^ (A,(i + 1))
then reconsider x = x, y = y as Element of A by ZFMISC_1:87;
reconsider a = Class (EP,y) as Element of P by A1, EQREL_1:def_3;
now__::_thesis:_for_f_being_operation_of_A
for_p,_q_being_FinSequence_st_(p_^_<*x*>)_^_q_in_dom_f_&_(p_^_<*y*>)_^_q_in_dom_f_holds_
[(f_._((p_^_<*x*>)_^_q)),(f_._((p_^_<*y*>)_^_q))]_in_(DomRel_A)_|^_(A,i)
let f be operation of A; ::_thesis: for p, q being FinSequence st (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f holds
[(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i)
let p, q be FinSequence; ::_thesis: ( (p ^ <*x*>) ^ q in dom f & (p ^ <*y*>) ^ q in dom f implies [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i) )
assume that
A13: (p ^ <*x*>) ^ q in dom f and
A14: (p ^ <*y*>) ^ q in dom f ; ::_thesis: [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i)
(p ^ <*x*>) ^ q is FinSequence of the carrier of A by A13, FINSEQ_1:def_11;
then consider pp being FinSequence of P such that
A15: (p ^ <*x*>) ^ q in product pp by Th7;
f is_exactly_partitable_wrt P by Def10;
then f is_partitable_wrt P by Def9;
then consider c being Element of P such that
A16: f .: (product pp) c= c by Def8;
A17: x in a by A12, EQREL_1:19;
y in a by EQREL_1:20;
then A18: (p ^ <*y*>) ^ q in product pp by A15, A17, Th26;
A19: f . ((p ^ <*x*>) ^ q) in f .: (product pp) by A13, A15, FUNCT_1:def_6;
A20: f . ((p ^ <*y*>) ^ q) in f .: (product pp) by A14, A18, FUNCT_1:def_6;
ex x being set st
( x in the carrier of A & c = Class (EP,x) ) by A1, EQREL_1:def_3;
then [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in EP by A16, A19, A20, EQREL_1:22;
hence [(f . ((p ^ <*x*>) ^ q)),(f . ((p ^ <*y*>) ^ q))] in (DomRel A) |^ (A,i) by A11; ::_thesis: verum
end;
then [x,y] in ((DomRel A) |^ (A,i)) |^ A by A11, A12, Def5;
hence [x,y] in (DomRel A) |^ (A,(i + 1)) by Th17; ::_thesis: verum
end;
A21: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A2, A10);
now__::_thesis:_for_i_being_Element_of_NAT_holds_[x,y]_in_(DomRel_A)_|^_(A,i)
let i be Element of NAT ; ::_thesis: [x,y] in (DomRel A) |^ (A,i)
ex x being set st
( x in the carrier of A & aa = Class (EP,x) ) by A1, EQREL_1:def_3;
then A22: [x,y] in EP by EQREL_1:22;
EP c= (DomRel A) |^ (A,i) by A21;
hence [x,y] in (DomRel A) |^ (A,i) by A22; ::_thesis: verum
end;
then [x,y] in LimDomRel A by Def7;
then [y,x] in LimDomRel A by EQREL_1:6;
hence y in Class ((LimDomRel A), the Element of aa) by EQREL_1:19; ::_thesis: verum
end;
begin
definition
let S1, S2 be ManySortedSign ;
let f, g be Function;
predf,g form_morphism_between S1,S2 means :Def12: :: PUA2MSS1:def 12
( dom f = the carrier of S1 & dom g = the carrier' of S1 & rng f c= the carrier of S2 & rng g c= the carrier' of S2 & f * the ResultSort of S1 = the ResultSort of S2 * g & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
f * p = the Arity of S2 . (g . o) ) );
end;
:: deftheorem Def12 defines form_morphism_between PUA2MSS1:def_12_:_
for S1, S2 being ManySortedSign
for f, g being Function holds
( f,g form_morphism_between S1,S2 iff ( dom f = the carrier of S1 & dom g = the carrier' of S1 & rng f c= the carrier of S2 & rng g c= the carrier' of S2 & f * the ResultSort of S1 = the ResultSort of S2 * g & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
f * p = the Arity of S2 . (g . o) ) ) );
theorem Th28: :: PUA2MSS1:28
for S being non empty non void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proof
let S be non empty non void ManySortedSign ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
set f = id the carrier of S;
set g = id the carrier' of S;
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
rng the ResultSort of S c= the carrier of S ;
then (id the carrier of S) * the ResultSort of S = the ResultSort of S by RELAT_1:53;
hence ( dom (id the carrier of S) = the carrier of S & dom (id the carrier' of S) = the carrier' of S & rng (id the carrier of S) c= the carrier of S & rng (id the carrier' of S) c= the carrier' of S & (id the carrier of S) * the ResultSort of S = the ResultSort of S * (id the carrier' of S) ) by A1, RELAT_1:52; :: according to PUA2MSS1:def_12 ::_thesis: for o being set
for p being Function st o in the carrier' of S & p = the Arity of S . o holds
(id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o)
let o be set ; ::_thesis: for p being Function st o in the carrier' of S & p = the Arity of S . o holds
(id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o)
let p be Function; ::_thesis: ( o in the carrier' of S & p = the Arity of S . o implies (id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o) )
assume that
A2: o in the carrier' of S and
A3: p = the Arity of S . o ; ::_thesis: (id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o)
A4: (id the carrier' of S) . o = o by A2, FUNCT_1:17;
p in the carrier of S * by A2, A3, FUNCT_2:5;
then p is FinSequence of the carrier of S by FINSEQ_1:def_11;
then rng p c= the carrier of S by FINSEQ_1:def_4;
hence (id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o) by A3, A4, RELAT_1:53; ::_thesis: verum
end;
theorem Th29: :: PUA2MSS1:29
for S1, S2, S3 being ManySortedSign
for f1, f2, g1, g2 being Function st f1,g1 form_morphism_between S1,S2 & f2,g2 form_morphism_between S2,S3 holds
f2 * f1,g2 * g1 form_morphism_between S1,S3
proof
let S1, S2, S3 be ManySortedSign ; ::_thesis: for f1, f2, g1, g2 being Function st f1,g1 form_morphism_between S1,S2 & f2,g2 form_morphism_between S2,S3 holds
f2 * f1,g2 * g1 form_morphism_between S1,S3
let f1, f2, g1, g2 be Function; ::_thesis: ( f1,g1 form_morphism_between S1,S2 & f2,g2 form_morphism_between S2,S3 implies f2 * f1,g2 * g1 form_morphism_between S1,S3 )
assume that
A1: dom f1 = the carrier of S1 and
A2: dom g1 = the carrier' of S1 and
A3: rng f1 c= the carrier of S2 and
A4: rng g1 c= the carrier' of S2 and
A5: f1 * the ResultSort of S1 = the ResultSort of S2 * g1 and
A6: for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
f1 * p = the Arity of S2 . (g1 . o) and
A7: dom f2 = the carrier of S2 and
A8: dom g2 = the carrier' of S2 and
A9: rng f2 c= the carrier of S3 and
A10: rng g2 c= the carrier' of S3 and
A11: f2 * the ResultSort of S2 = the ResultSort of S3 * g2 and
A12: for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f2 * p = the Arity of S3 . (g2 . o) ; :: according to PUA2MSS1:def_12 ::_thesis: f2 * f1,g2 * g1 form_morphism_between S1,S3
set f = f2 * f1;
set g = g2 * g1;
thus ( dom (f2 * f1) = the carrier of S1 & dom (g2 * g1) = the carrier' of S1 ) by A1, A2, A3, A4, A7, A8, RELAT_1:27; :: according to PUA2MSS1:def_12 ::_thesis: ( rng (f2 * f1) c= the carrier of S3 & rng (g2 * g1) c= the carrier' of S3 & (f2 * f1) * the ResultSort of S1 = the ResultSort of S3 * (g2 * g1) & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o) ) )
A13: rng (f2 * f1) c= rng f2 by RELAT_1:26;
rng (g2 * g1) c= rng g2 by RELAT_1:26;
hence ( rng (f2 * f1) c= the carrier of S3 & rng (g2 * g1) c= the carrier' of S3 ) by A9, A10, A13, XBOOLE_1:1; ::_thesis: ( (f2 * f1) * the ResultSort of S1 = the ResultSort of S3 * (g2 * g1) & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o) ) )
thus (f2 * f1) * the ResultSort of S1 = f2 * ( the ResultSort of S2 * g1) by A5, RELAT_1:36
.= (f2 * the ResultSort of S2) * g1 by RELAT_1:36
.= the ResultSort of S3 * (g2 * g1) by A11, RELAT_1:36 ; ::_thesis: for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o)
let o be set ; ::_thesis: for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o)
let p be Function; ::_thesis: ( o in the carrier' of S1 & p = the Arity of S1 . o implies (f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o) )
assume that
A14: o in the carrier' of S1 and
A15: p = the Arity of S1 . o ; ::_thesis: (f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o)
A16: f1 * p = the Arity of S2 . (g1 . o) by A6, A14, A15;
A17: g1 . o in rng g1 by A2, A14, FUNCT_1:def_3;
A18: (f2 * f1) * p = f2 * (f1 * p) by RELAT_1:36;
(g2 * g1) . o = g2 . (g1 . o) by A2, A14, FUNCT_1:13;
hence (f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o) by A4, A12, A16, A17, A18; ::_thesis: verum
end;
definition
let S1, S2 be ManySortedSign ;
predS1 is_rougher_than S2 means :: PUA2MSS1:def 13
ex f, g being Function st
( f,g form_morphism_between S2,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1 );
end;
:: deftheorem defines is_rougher_than PUA2MSS1:def_13_:_
for S1, S2 being ManySortedSign holds
( S1 is_rougher_than S2 iff ex f, g being Function st
( f,g form_morphism_between S2,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1 ) );
definition
let S1, S2 be non empty non void ManySortedSign ;
:: original: is_rougher_than
redefine predS1 is_rougher_than S2;
reflexivity
for S1 being non empty non void ManySortedSign holds (b1,b1)
proof
let S be non empty non void ManySortedSign ; ::_thesis: (S,S)
take f = id the carrier of S; :: according to PUA2MSS1:def_13 ::_thesis: ex g being Function st
( f,g form_morphism_between S,S & rng f = the carrier of S & rng g = the carrier' of S )
take g = id the carrier' of S; ::_thesis: ( f,g form_morphism_between S,S & rng f = the carrier of S & rng g = the carrier' of S )
thus ( f,g form_morphism_between S,S & rng f = the carrier of S & rng g = the carrier' of S ) by Th28, RELAT_1:45; ::_thesis: verum
end;
end;
theorem :: PUA2MSS1:30
for S1, S2, S3 being ManySortedSign st S1 is_rougher_than S2 & S2 is_rougher_than S3 holds
S1 is_rougher_than S3
proof
let S1, S2, S3 be ManySortedSign ; ::_thesis: ( S1 is_rougher_than S2 & S2 is_rougher_than S3 implies S1 is_rougher_than S3 )
given f1, g1 being Function such that A1: f1,g1 form_morphism_between S2,S1 and
A2: rng f1 = the carrier of S1 and
A3: rng g1 = the carrier' of S1 ; :: according to PUA2MSS1:def_13 ::_thesis: ( not S2 is_rougher_than S3 or S1 is_rougher_than S3 )
given f2, g2 being Function such that A4: f2,g2 form_morphism_between S3,S2 and
A5: rng f2 = the carrier of S2 and
A6: rng g2 = the carrier' of S2 ; :: according to PUA2MSS1:def_13 ::_thesis: S1 is_rougher_than S3
take f = f1 * f2; :: according to PUA2MSS1:def_13 ::_thesis: ex g being Function st
( f,g form_morphism_between S3,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1 )
take g = g1 * g2; ::_thesis: ( f,g form_morphism_between S3,S1 & rng f = the carrier of S1 & rng g = the carrier' of S1 )
thus f,g form_morphism_between S3,S1 by A1, A4, Th29; ::_thesis: ( rng f = the carrier of S1 & rng g = the carrier' of S1 )
A7: dom f1 = the carrier of S2 by A1, Def12;
dom g1 = the carrier' of S2 by A1, Def12;
hence ( rng f = the carrier of S1 & rng g = the carrier' of S1 ) by A2, A3, A5, A6, A7, RELAT_1:28; ::_thesis: verum
end;
begin
definition
let A be partial non-empty UAStr ;
let P be a_partition of A;
func MSSign (A,P) -> strict ManySortedSign means :Def14: :: PUA2MSS1:def 14
( the carrier of it = P & the carrier' of it = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of it . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of it . [o,p] ) ) );
existence
ex b1 being strict ManySortedSign st
( the carrier of b1 = P & the carrier' of b1 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of b1 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b1 . [o,p] ) ) )
proof
set O = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ;
defpred S1[ set , set ] means ex f being OperSymbol of A ex q being Element of P * st
( q = $2 & $1 = [f,q] );
A1: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } holds
ex p being set st
( p in P * & S1[o,p] )
proof
let o be set ; ::_thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } implies ex p being set st
( p in P * & S1[o,p] ) )
assume o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ; ::_thesis: ex p being set st
( p in P * & S1[o,p] )
then consider f being OperSymbol of A, p being Element of P * such that
A2: o = [f,p] and
product p meets dom (Den (f,A)) ;
take p ; ::_thesis: ( p in P * & S1[o,p] )
thus ( p in P * & S1[o,p] ) by A2; ::_thesis: verum
end;
defpred S2[ set , set ] means ex f being OperSymbol of A ex p being Element of P * st
( $1 = [f,p] & (Den (f,A)) .: (product p) c= $2 );
A3: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } holds
ex r being set st
( r in P & S2[o,r] )
proof
let o be set ; ::_thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } implies ex r being set st
( r in P & S2[o,r] ) )
assume o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ; ::_thesis: ex r being set st
( r in P & S2[o,r] )
then consider f being OperSymbol of A, p being Element of P * such that
A4: o = [f,p] and
product p meets dom (Den (f,A)) ;
Den (f,A) is_exactly_partitable_wrt P by Def10;
then Den (f,A) is_partitable_wrt P by Def9;
then ex a being Element of P st (Den (f,A)) .: (product p) c= a by Def8;
hence ex r being set st
( r in P & S2[o,r] ) by A4; ::_thesis: verum
end;
consider Ar being Function such that
A5: ( dom Ar = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } & rng Ar c= P * ) and
A6: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } holds
S1[o,Ar . o] from FUNCT_1:sch_5(A1);
reconsider Ar = Ar as Function of { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ,(P *) by A5, FUNCT_2:2;
consider R being Function such that
A7: ( dom R = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } & rng R c= P ) and
A8: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } holds
S2[o,R . o] from FUNCT_1:sch_5(A3);
reconsider R = R as Function of { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ,P by A7, FUNCT_2:2;
take S = ManySortedSign(# P, { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ,Ar,R #); ::_thesis: ( the carrier of S = P & the carrier' of S = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of S . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of S . [o,p] ) ) )
thus ( the carrier of S = P & the carrier' of S = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ) ; ::_thesis: for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of S . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of S . [o,p] )
let f be OperSymbol of A; ::_thesis: for p being Element of P * st product p meets dom (Den (f,A)) holds
( the Arity of S . [f,p] = p & (Den (f,A)) .: (product p) c= the ResultSort of S . [f,p] )
let p be Element of P * ; ::_thesis: ( product p meets dom (Den (f,A)) implies ( the Arity of S . [f,p] = p & (Den (f,A)) .: (product p) c= the ResultSort of S . [f,p] ) )
set o = [f,p];
assume product p meets dom (Den (f,A)) ; ::_thesis: ( the Arity of S . [f,p] = p & (Den (f,A)) .: (product p) c= the ResultSort of S . [f,p] )
then A9: [f,p] in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ;
then A10: ex f1 being OperSymbol of A ex q1 being Element of P * st
( q1 = Ar . [f,p] & [f,p] = [f1,q1] ) by A6;
consider f2 being OperSymbol of A, q2 being Element of P * such that
A11: [f,p] = [f2,q2] and
A12: (Den (f2,A)) .: (product q2) c= R . [f,p] by A8, A9;
q2 = p by A11, XTUPLE_0:1;
hence ( the Arity of S . [f,p] = p & (Den (f,A)) .: (product p) c= the ResultSort of S . [f,p] ) by A10, A11, A12, XTUPLE_0:1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict ManySortedSign st the carrier of b1 = P & the carrier' of b1 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of b1 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b1 . [o,p] ) ) & the carrier of b2 = P & the carrier' of b2 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of b2 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b2 . [o,p] ) ) holds
b1 = b2;
proof
set O = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ;
let S1, S2 be strict ManySortedSign ; ::_thesis: ( the carrier of S1 = P & the carrier' of S1 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of S1 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of S1 . [o,p] ) ) & the carrier of S2 = P & the carrier' of S2 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of S2 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of S2 . [o,p] ) ) implies S1 = S2 )
assume that
A13: the carrier of S1 = P and
A14: the carrier' of S1 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } and
A15: for f being OperSymbol of A
for p being Element of P * st product p meets dom (Den (f,A)) holds
( the Arity of S1 . [f,p] = p & (Den (f,A)) .: (product p) c= the ResultSort of S1 . [f,p] ) and
A16: the carrier of S2 = P and
A17: the carrier' of S2 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } and
A18: for f being OperSymbol of A
for p being Element of P * st product p meets dom (Den (f,A)) holds
( the Arity of S2 . [f,p] = p & (Den (f,A)) .: (product p) c= the ResultSort of S2 . [f,p] ) ; ::_thesis: S1 = S2
A19: dom the Arity of S1 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } by A14, FUNCT_2:def_1;
A20: dom the Arity of S2 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } by A17, FUNCT_2:def_1;
now__::_thesis:_for_o_being_set_st_o_in__{__[f,p]_where_f_is_OperSymbol_of_A,_p_is_Element_of_P_*_:_product_p_meets_dom_(Den_(f,A))__}__holds_
the_Arity_of_S1_._o_=_the_Arity_of_S2_._o
let o be set ; ::_thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } implies the Arity of S1 . o = the Arity of S2 . o )
assume o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ; ::_thesis: the Arity of S1 . o = the Arity of S2 . o
then consider f being OperSymbol of A, p being Element of P * such that
A21: o = [f,p] and
A22: product p meets dom (Den (f,A)) ;
thus the Arity of S1 . o = p by A15, A21, A22
.= the Arity of S2 . o by A18, A21, A22 ; ::_thesis: verum
end;
then A23: the Arity of S1 = the Arity of S2 by A19, A20, FUNCT_1:2;
A24: dom the ResultSort of S1 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } by A13, A14, FUNCT_2:def_1;
A25: dom the ResultSort of S2 = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } by A16, A17, FUNCT_2:def_1;
consider R being Equivalence_Relation of the carrier of A such that
A26: P = Class R by EQREL_1:34;
now__::_thesis:_for_o_being_set_st_o_in__{__[f,p]_where_f_is_OperSymbol_of_A,_p_is_Element_of_P_*_:_product_p_meets_dom_(Den_(f,A))__}__holds_
the_ResultSort_of_S1_._o_=_the_ResultSort_of_S2_._o
let o be set ; ::_thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } implies the ResultSort of S1 . o = the ResultSort of S2 . o )
assume A27: o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } ; ::_thesis: the ResultSort of S1 . o = the ResultSort of S2 . o
then consider f being OperSymbol of A, p being Element of P * such that
A28: o = [f,p] and
A29: product p meets dom (Den (f,A)) ;
consider x being set such that
A30: x in product p and
A31: x in dom (Den (f,A)) by A29, XBOOLE_0:3;
A32: (Den (f,A)) . x in (Den (f,A)) .: (product p) by A30, A31, FUNCT_1:def_6;
A33: (Den (f,A)) .: (product p) c= the ResultSort of S1 . o by A15, A28, A29;
A34: (Den (f,A)) .: (product p) c= the ResultSort of S2 . o by A18, A28, A29;
A35: the ResultSort of S1 . o in P by A13, A14, A27, FUNCT_2:5;
A36: the ResultSort of S2 . o in P by A16, A17, A27, FUNCT_2:5;
A37: ex y being set st
( y in the carrier of A & the ResultSort of S1 . o = Class (R,y) ) by A26, A35, EQREL_1:def_3;
A38: ex y being set st
( y in the carrier of A & the ResultSort of S2 . o = Class (R,y) ) by A26, A36, EQREL_1:def_3;
the ResultSort of S1 . o = Class (R,((Den (f,A)) . x)) by A32, A33, A37, EQREL_1:23;
hence the ResultSort of S1 . o = the ResultSort of S2 . o by A32, A34, A38, EQREL_1:23; ::_thesis: verum
end;
hence S1 = S2 by A13, A14, A16, A17, A23, A24, A25, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines MSSign PUA2MSS1:def_14_:_
for A being partial non-empty UAStr
for P being a_partition of A
for b3 being strict ManySortedSign holds
( b3 = MSSign (A,P) iff ( the carrier of b3 = P & the carrier' of b3 = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den (o,A)) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den (o,A)) holds
( the Arity of b3 . [o,p] = p & (Den (o,A)) .: (product p) c= the ResultSort of b3 . [o,p] ) ) ) );
registration
let A be partial non-empty UAStr ;
let P be a_partition of A;
cluster MSSign (A,P) -> non empty non void strict ;
coherence
( not MSSign (A,P) is empty & not MSSign (A,P) is void )
proof
thus not the carrier of (MSSign (A,P)) is empty by Def14; :: according to STRUCT_0:def_1 ::_thesis: not MSSign (A,P) is void
set g = the OperSymbol of A;
set x = the Element of dom (Den ( the OperSymbol of A,A));
reconsider x = the Element of dom (Den ( the OperSymbol of A,A)) as Element of the carrier of A * ;
A1: union P = the carrier of A by EQREL_1:def_4;
rng x c= the carrier of A ;
then consider q being Function such that
A2: dom q = dom x and
A3: rng q c= P and
A4: x in product q by A1, Th6;
dom x = Seg (len x) by FINSEQ_1:def_3;
then reconsider q = q as FinSequence by A2, FINSEQ_1:def_2;
reconsider q = q as FinSequence of P by A3, FINSEQ_1:def_4;
reconsider q = q as Element of P * by FINSEQ_1:def_11;
A5: product q meets dom (Den ( the OperSymbol of A,A)) by A4, XBOOLE_0:3;
the carrier' of (MSSign (A,P)) = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } by Def14;
then [ the OperSymbol of A,q] in the carrier' of (MSSign (A,P)) by A5;
hence not the carrier' of (MSSign (A,P)) is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;
definition
let A be partial non-empty UAStr ;
let P be a_partition of A;
let o be OperSymbol of (MSSign (A,P));
:: original: `1
redefine funco `1 -> OperSymbol of A;
coherence
o `1 is OperSymbol of A
proof
A1: o in the carrier' of (MSSign (A,P)) ;
the carrier' of (MSSign (A,P)) = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } by Def14;
then ex f being OperSymbol of A ex p being Element of P * st
( o = [f,p] & product p meets dom (Den (f,A)) ) by A1;
hence o `1 is OperSymbol of A by MCART_1:7; ::_thesis: verum
end;
:: original: `2
redefine funco `2 -> Element of P * ;
coherence
o `2 is Element of P *
proof
A2: o in the carrier' of (MSSign (A,P)) ;
the carrier' of (MSSign (A,P)) = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den (f,A)) } by Def14;
then ex f being OperSymbol of A ex p being Element of P * st
( o = [f,p] & product p meets dom (Den (f,A)) ) by A2;
hence o `2 is Element of P * by MCART_1:7; ::_thesis: verum
end;
end;
definition
let A be partial non-empty UAStr ;
let S be non empty non void ManySortedSign ;
let G be MSAlgebra over S;
let P be IndexedPartition of the carrier' of S;
predA can_be_characterized_by S,G,P means :Def15: :: PUA2MSS1:def 15
( the Sorts of G is IndexedPartition of A & dom P = dom the charact of A & ( for o being OperSymbol of A holds the Charact of G | (P . o) is IndexedPartition of Den (o,A) ) );
end;
:: deftheorem Def15 defines can_be_characterized_by PUA2MSS1:def_15_:_
for A being partial non-empty UAStr
for S being non empty non void ManySortedSign
for G being MSAlgebra over S
for P being IndexedPartition of the carrier' of S holds
( A can_be_characterized_by S,G,P iff ( the Sorts of G is IndexedPartition of A & dom P = dom the charact of A & ( for o being OperSymbol of A holds the Charact of G | (P . o) is IndexedPartition of Den (o,A) ) ) );
definition
let A be partial non-empty UAStr ;
let S be non empty non void ManySortedSign ;
predA can_be_characterized_by S means :: PUA2MSS1:def 16
ex G being MSAlgebra over S ex P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P;
end;
:: deftheorem defines can_be_characterized_by PUA2MSS1:def_16_:_
for A being partial non-empty UAStr
for S being non empty non void ManySortedSign holds
( A can_be_characterized_by S iff ex G being MSAlgebra over S ex P being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,P );
theorem :: PUA2MSS1:31
for A being partial non-empty UAStr
for P being a_partition of A holds A can_be_characterized_by MSSign (A,P)
proof
let A be partial non-empty UAStr ; ::_thesis: for P being a_partition of A holds A can_be_characterized_by MSSign (A,P)
let P be a_partition of A; ::_thesis: 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 V16()
proof
let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in proj1 Q or not Q . x is empty )
assume x in dom Q ; ::_thesis: 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, Th6;
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 ; ::_thesis: 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 set ; :: according to PBOOLE:def_15 ::_thesis: ( 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)) ; ::_thesis: 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, MCART_1:7;
A23: xx `1 = o by A13, MCART_1:7;
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, Def9;
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; ::_thesis: 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))
proof
hereby :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis: the carrier' of (MSSign (A,P)) c= Union Q
let x be set ; ::_thesis: ( x in Union Q implies x in the carrier' of (MSSign (A,P)) )
assume x in Union Q ; ::_thesis: x in the carrier' of (MSSign (A,P))
then consider y being set such that
A29: y in dom Q and
A30: x in Q . y by CARD_5:2;
reconsider y = y as OperSymbol of A by A29, PARTFUN1:def_2;
Q . y = { a where a is OperSymbol of (MSSign (A,P)) : a `1 = y } by A2;
then ex a being OperSymbol of (MSSign (A,P)) st
( x = a & a `1 = y ) by A30;
hence x in the carrier' of (MSSign (A,P)) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of (MSSign (A,P)) or x in Union Q )
assume x in the carrier' of (MSSign (A,P)) ; ::_thesis: x in Union Q
then reconsider b = x as OperSymbol of (MSSign (A,P)) ;
Q . (b `1) = { a where a is OperSymbol of (MSSign (A,P)) : a `1 = b `1 } by A2;
then b in Q . (b `1) ;
hence x in Union Q by A3, CARD_5:2; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_Q_&_y_in_dom_Q_&_x_<>_y_holds_
Q_._x_misses_Q_._y
let x, y be set ; ::_thesis: ( x in dom Q & y in dom Q & x <> y implies Q . x misses Q . y )
assume that
A31: x in dom Q and
A32: y in dom Q and
A33: x <> y ; ::_thesis: Q . x misses Q . y
reconsider a = x, b = y as OperSymbol of A by A31, A32, PARTFUN1:def_2;
thus Q . x misses Q . y ::_thesis: verum
proof
assume Q . x meets Q . y ; ::_thesis: contradiction
then consider z being set such that
A34: z in Q . x and
A35: z in Q . y by XBOOLE_0:3;
A36: Q . a = { c where c is OperSymbol of (MSSign (A,P)) : c `1 = a } by A2;
A37: Q . b = { c where c is OperSymbol of (MSSign (A,P)) : c `1 = b } by A2;
A38: ex c1 being OperSymbol of (MSSign (A,P)) st
( z = c1 & c1 `1 = a ) by A34, A36;
ex c2 being OperSymbol of (MSSign (A,P)) st
( z = c2 & c2 `1 = b ) by A35, A37;
hence contradiction by A33, A38; ::_thesis: verum
end;
end;
then reconsider Q = Q as IndexedPartition of the carrier' of (MSSign (A,P)) by A28, Th14;
take G = MSAlgebra(# Z,D #); :: according to PUA2MSS1:def_16 ::_thesis: ex P being IndexedPartition of the carrier' of (MSSign (A,P)) st A can_be_characterized_by MSSign (A,P),G,P
take Q ; ::_thesis: 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; :: according to PUA2MSS1:def_15 ::_thesis: ( 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; ::_thesis: 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; ::_thesis: 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 Th9;
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 Th11;
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 Th12;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in RR )
assume y in rng F ; ::_thesis: y in RR
then consider x being set 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, MCART_1:7;
A50: a `2 = p by A47, MCART_1:7;
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, Def9;
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; ::_thesis: 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in RR or x in rng F )
assume x in RR ; ::_thesis: 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, Def9;
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; ::_thesis: verum
end;
F is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( 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 ; ::_thesis: 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, MCART_1:7;
A80: a2 `2 = p2 by A75, MCART_1:7;
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, MCART_1:7;
A85: o = o2 by A72, A75, MCART_1:7;
A86: product p1 c= dom (Den (o,A)) by A74, A83, A84, Def9;
A87: product p2 c= dom (Den (o,A)) by A76, A83, A85, Def9;
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; ::_thesis: verum
end;
hence the Charact of G | (Q . o) is IndexedPartition of Den (o,A) by A55, Th15; ::_thesis: verum
end;
theorem Th32: :: PUA2MSS1:32
for A being partial non-empty UAStr
for S being non empty non void ManySortedSign
for G being MSAlgebra over S
for Q being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
proof
let A be partial non-empty UAStr ; ::_thesis: for S being non empty non void ManySortedSign
for G being MSAlgebra over S
for Q being IndexedPartition of the carrier' of S st A can_be_characterized_by S,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let S2 be non empty non void ManySortedSign ; ::_thesis: for G being MSAlgebra over S2
for Q being IndexedPartition of the carrier' of S2 st A can_be_characterized_by S2,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let G be MSAlgebra over S2; ::_thesis: for Q being IndexedPartition of the carrier' of S2 st A can_be_characterized_by S2,G,Q holds
for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let Q be IndexedPartition of the carrier' of S2; ::_thesis: ( A can_be_characterized_by S2,G,Q implies for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o ) )
assume that
A1: the Sorts of G is IndexedPartition of A and
A2: dom Q = dom the charact of A and
A3: for o being OperSymbol of A holds the Charact of G | (Q . o) is IndexedPartition of Den (o,A) ; :: according to PUA2MSS1:def_15 ::_thesis: for o being OperSymbol of A
for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
reconsider R = the Sorts of G as IndexedPartition of A by A1;
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;
let o be OperSymbol of A; ::_thesis: for r being FinSequence of rng the Sorts of G st product r c= dom (Den (o,A)) holds
ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
let r be FinSequence of rng the Sorts of G; ::_thesis: ( product r c= dom (Den (o,A)) implies ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o ) )
reconsider p = r as Element of (rng R) * by FINSEQ_1:def_11;
assume A4: product r c= dom (Den (o,A)) ; ::_thesis: ex s being OperSymbol of S2 st
( the Sorts of G * (the_arity_of s) = r & s in Q . o )
reconsider P = the Charact of G | (Q . o) as IndexedPartition of Den (o,A) by A3;
set h = the Element of product p;
the Element of product p in product r ;
then A5: [ the Element of product p,((Den (o,A)) . the Element of product p)] in Den (o,A) by A4, FUNCT_1:def_2;
then A6: P -index_of [ the Element of product p,((Den (o,A)) . the Element of product p)] in dom P by Def3;
A7: [ the Element of product p,((Den (o,A)) . the Element of product p)] in P . (P -index_of [ the Element of product p,((Den (o,A)) . the Element of product p)]) by A5, Def3;
reconsider Qo = Q . o as Element of rng Q by A2, FUNCT_1:def_3;
A8: dom the Charact of G = the carrier' of S2 by PARTFUN1:def_2;
then A9: dom P = Qo by RELAT_1:62;
reconsider s = P -index_of [ the Element of product p,((Den (o,A)) . the Element of product p)] as Element of Qo by A6, A8, RELAT_1:62;
reconsider q = SG * (the_arity_of s) as FinSequence of rng R by Lm2;
reconsider q = q as Element of (rng R) * by FINSEQ_1:def_11;
reconsider Q = { (product t) where t is Element of (rng R) * : verum } as a_partition of the carrier of A * by Th9;
take s ; ::_thesis: ( the Sorts of G * (the_arity_of s) = r & s in Q . o )
dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
then A10: Args (s,G) = ( the Sorts of G #) . ( the Arity of S2 . s) by FUNCT_1:13
.= product q by FINSEQ_2:def_5 ;
A11: product q in Q ;
A12: product p in Q ;
P . s = the Charact of G . s by A9, FUNCT_1:47;
then the Element of product p in dom (Den (s,G)) by A7, XTUPLE_0:def_12;
hence the Sorts of G * (the_arity_of s) = r by A10, A11, A12, Th2, Lm3; ::_thesis: s in Q . o
thus s in Q . o ; ::_thesis: verum
end;
theorem :: PUA2MSS1:33
for A being 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
proof
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, Def15;
A4: dom Q = dom the charact of A by A2, Def15;
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, Def15;
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[ set , set ] means $1 c= $2;
A8: rng R is_finer_than P by A1, Th27;
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 FUNCT_1:sch_5(A9);
reconsider em = em as Function of (rng R),P by A10, FUNCT_2:2;
A12: dom (em * R) = dom R by A10, RELAT_1:27;
rng (em * R) = rng em by A10, RELAT_1:28;
then reconsider f = em * R as Function of the carrier of S2, the carrier of (MSSign (A,P)) by A5, A7, A12, 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[ 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 ; ::_thesis: ( 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 ; ::_thesis: 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, Th27;
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);
A15: the Element of Args (s2,G) 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_2;
A18: 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, Def15;
then rng ( the Charact of G | (Q . o)) is a_partition of Den (o,A) by Def2;
then A19: 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 A18, FUNCT_1:def_6;
then A20: dom (Den (s2,G)) c= dom (Den (o,A)) by A19, RELAT_1:11;
A21: Args (s2,G) = ( the Sorts of G #) . ( the Arity of S2 . s2) by A17, FUNCT_1:13
.= product (SG * (the_arity_of s2)) by FINSEQ_2:def_5 ;
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; ::_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 A14, A21; ::_thesis: 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 FUNCT_1:sch_5(A13);
reconsider g = g as Function of the carrier' of S2, the carrier' of (MSSign (A,P)) by A22, 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 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; :: 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;
A24: R . ( the ResultSort of S2 . c) = ( the Sorts of G * the ResultSort of S2) . c by FUNCT_2:15;
A25: (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 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:13;
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, Def3;
set aa = the Element of Args (o,G);
the Charact of G | (Q . s2) is IndexedPartition of Den (s2,A) by A2, Def15;
then A30: rng ( the Charact of G | (Q . s2)) is a_partition of Den (s2,A) by Def2;
A31: o in Q . s2 by A28, Def3;
A32: dom the Charact of G = the carrier' of S2 by PARTFUN1:def_2;
A33: the Charact of G .: (Q . s2) is a_partition of Den (s2,A) by A30, RELAT_1:115;
A34: the Charact of G . o in the Charact of G .: (Q . s2) by A31, A32, FUNCT_1:def_6;
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:11;
the Element of Args (o,G) 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, Def14;
rng (Den (c,G)) = (Den (c,G)) .: (Args (c,G)) by A28, A35, RELAT_1:113;
then A38: rng (Den (c,G)) c= (Den (c,G)) .: (product p) by A28, A29, RELAT_1:123;
(Den (c,G)) .: (product p) c= (Den (s2,A)) .: (product p) by A28, A33, A34, RELAT_1:124;
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)) . the Element of Args (o,G) in rng (Den (c,G)) by A28, A35, FUNCT_1:def_3;
then A41: (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 A39, A40;
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, A24, A25, A26, A41, Lm3; ::_thesis: verum
end;
hence f * the ResultSort of S2 = the ResultSort of (MSSign (A,P)) * g by FUNCT_2:63; ::_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 A42: 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
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, XTUPLE_0:1;
then A48: the Arity of (MSSign (A,P)) . (g . o) = p9 by A46, A47, Def14;
Args (o9,G) = ( the Sorts of G #) . q by A44, FUNCT_2:15
.= product r by FINSEQ_2:def_5 ;
then em * r = p9 by A11, A45, Th5;
hence f * p = the Arity of (MSSign (A,P)) . (g . o) by A42, A48, 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 set ; :: 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;
A49: R -index_of the Element of s in dom R by Def3;
A50: the Element of s in R . (R -index_of the Element of s) by Def3;
A51: R . (R -index_of the Element of s) in rng R by A49, FUNCT_1:def_3;
em . (R . (R -index_of the Element of s)) = f . (R -index_of the Element of s) by A49, FUNCT_1:13;
then A52: R . (R -index_of the Element of s) c= f . (R -index_of the Element of s) by A11, A51;
A53: f . (R -index_of the Element of s) in rng f by A5, A23, A49, FUNCT_1:def_3;
rng f c= P by A23, Def14;
hence s in rng f by A50, A52, A53, 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 set ; :: 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
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:1;
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:77;
union P = the carrier of A by EQREL_1:def_4;
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:9;
A65: Den (o,A) is_exactly_partitable_wrt P by Def10;
now__::_thesis:_for_x_being_set_st_x_in_dom_r_holds_
r_._x_c=_p_._x
let x be set ; ::_thesis: ( x in dom r implies r . x c= p . x )
assume A66: x in dom r ; ::_thesis: r . x c= p . x
then A67: h . x in p . x by A58, A59, A64;
A68: h . x in r . x by A63, A66, CARD_3:9;
A69: r . x in rng r by A66, FUNCT_1:def_3;
A70: p . x in rng p by A58, A64, A66, FUNCT_1:def_3;
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, Lm3; ::_thesis: verum
end;
then A71: product r c= product p by A58, A64, CARD_3:27;
product p c= dom (Den (o,A)) by A55, A65, Def9;
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, Th32, 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:13
.= product r by A72, FINSEQ_2:def_5 ;
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, Def3;
hence s1 in rng g by A22, A54, A74, A77, A78, FUNCT_1:def_3; ::_thesis: verum
end;
end;