:: 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;