### The Mizar article:

### Minimal Signature for Partial Algebra

**by****Grzegorz Bancerek**

- Received October 1, 1995
Copyright (c) 1995 Association of Mizar Users

- MML identifier: PUA2MSS1
- [ MML identifier index ]

environ vocabulary RELAT_1, FINSEQ_1, FUNCT_1, ZF_REFLE, AMI_1, BOOLE, PARTFUN1, UNIALG_1, FUNCT_2, CARD_3, MSUALG_1, UNIALG_2, EQREL_1, SETFAM_1, TARSKI, FINSEQ_2, PROB_1, PBOOLE, INCPROJ, RELAT_2, GROUP_1, MCART_1, PRALG_1, TDGROUP, QC_LANG1, PUA2MSS1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, SETFAM_1, RELAT_1, STRUCT_0, RELSET_1, FUNCT_1, MCART_1, FINSEQ_1, FINSEQ_2, PARTFUN1, FUNCT_2, RELAT_2, EQREL_1, AMI_1, PROB_1, CARD_3, PBOOLE, MSUALG_1, UNIALG_1; constructors NAT_1, PRVECT_1, EQREL_1, AMI_1, MSUALG_1, PROB_1, MEMBERED, PARTFUN1, RELAT_1, RELAT_2; clusters SUBSET_1, STRUCT_0, RELSET_1, FUNCT_1, AMI_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, UNIALG_1, PRVECT_1, MSUALG_1, MSAFREE, FSM_1, PARTFUN1, NAT_1, FRAENKEL, RELAT_1, EQREL_1, TOLER_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; definitions STRUCT_0, XBOOLE_0, TARSKI, SETFAM_1, RELAT_1, FUNCT_1, RELAT_2, EQREL_1, AMI_1, UNIALG_1, MSUALG_1; theorems TARSKI, ZFMISC_1, MCART_1, SETFAM_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_2, AMI_1, EQREL_1, CARD_3, FUNCT_2, PARTFUN1, PROB_1, CARD_5, UNIALG_1, PBOOLE, FUNCT_6, MSUALG_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, RELAT_2, ORDERS_1; schemes NAT_1, RECDEF_1, RELSET_1, PARTFUN1, PRALG_2, COMPTS_1; begin :: Preliminary ::------------------------------------------------------------------- :: Acknowledgements: :: ================ :: :: I would like to thank Professor Andrzej Trybulec for suggesting me :: the problem solved here. ::------------------------------------------------------------------- Lm1: for p being FinSequence, f being Function st dom f = dom p holds f is FinSequence proof let p be FinSequence; dom p = Seg len p by FINSEQ_1:def 3; hence thesis by FINSEQ_1:def 2; end; Lm2: for X being set, Y being non empty set for p being FinSequence of X, f being Function of X,Y holds f*p is FinSequence of Y proof let X be set, Y be non empty set; let p be FinSequence of X, f be Function of X,Y; rng p c= X & dom f = X by FINSEQ_1:def 4,FUNCT_2:def 1; then dom (f*p) = dom p & rng f c= Y & rng (f*p) c= rng f by RELAT_1:45,46,RELSET_1:12; then f*p is FinSequence & rng (f*p) c= Y by Lm1,XBOOLE_1:1; hence thesis by FINSEQ_1:def 4; end; definition let f be non-empty Function; cluster rng f -> with_non-empty_elements; coherence proof assume {} in rng f; then ex x being set st x in dom f & {} = f.x by FUNCT_1:def 5; hence thesis by UNIALG_1:def 6; end; end; definition let X,Y be non empty set; cluster non empty PartFunc of X,Y; existence proof consider f being non empty PartFunc of Y*,Y; consider g being Function of X, dom f; A1: dom g = X & rng g c= dom f & dom f c= Y* by FUNCT_2:def 1,RELSET_1:12; then rng g c= Y* by XBOOLE_1:1; then reconsider g as PartFunc of X, Y* by A1,PARTFUN1:25; take f*g; consider x being Element of X; g.x in dom f by FUNCT_2:7; then x in dom (f*g) by A1,FUNCT_1:21; then [x, (f*g).x] in f*g by FUNCT_1:8; hence thesis; end; end; definition let X be with_non-empty_elements set; cluster -> non-empty FinSequence of X; coherence proof let p be FinSequence of X; let x be set; assume x in dom p; then p.x in rng p & rng p c= X by FINSEQ_1:def 4,FUNCT_1:def 5; hence thesis by AMI_1:def 1; end; end; definition let A be non empty set; cluster homogeneous quasi_total non-empty non empty PFuncFinSequence of A; existence proof consider a being homogeneous quasi_total non empty PartFunc of A*,A; reconsider a as Element of PFuncs(A*,A) by PARTFUN1:119; take <*a*>; hereby let n be Nat, h be PartFunc of A*,A; assume n in dom <*a*>; then n in Seg 1 by FINSEQ_1:55; then n = 1 by FINSEQ_1:4,TARSKI:def 1; hence h = <*a*>.n implies h is homogeneous by FINSEQ_1:57; end; hereby let n be Nat, h be PartFunc of A*,A; assume n in dom <*a*>; then n in Seg 1 by FINSEQ_1:55; then n = 1 by FINSEQ_1:4,TARSKI:def 1; hence h = <*a*>.n implies h is quasi_total by FINSEQ_1:57; end; hereby let n be set; assume n in dom <*a*>; then n in Seg 1 by FINSEQ_1:55; then n = 1 by FINSEQ_1:4,TARSKI:def 1; hence <*a*>.n is non empty by FINSEQ_1:57; end; thus thesis; end; end; definition cluster non-empty -> non empty UAStr; coherence proof let A be UAStr; assume A1: the charact of A <> {} & the charact of A is non-empty; then reconsider f = the charact of A as non empty Function; consider x being Element of dom f; reconsider y = f.x as non empty set by A1,UNIALG_1:def 6; A2: y in rng f & rng f c= PFuncs((the carrier of A)*, the carrier of A) by FINSEQ_1:def 4,FUNCT_1:def 5; then A3: y is PartFunc of (the carrier of A)*, the carrier of A by PARTFUN1:121; reconsider y as non empty Function by A2,PARTFUN1:121; consider z being Element of rng y; z in rng y & rng y c= the carrier of A by A3,RELSET_1:12; hence the carrier of A is non empty; end; end; definition let X be non empty with_non-empty_elements set; cluster -> non empty Element of X; coherence by AMI_1:def 1; end; theorem Th1: 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; assume A1: product f c= product g; consider h being Element of product f; h in product f; then A2: (ex i being Function st h = i & dom i = dom g & for x being set st x in dom g holds i.x in g.x) & ex i being Function st h = i & dom i = dom f & for x being set st x in dom f holds i.x in f.x by A1,CARD_3:def 5; hence dom f = dom g; let x be set; assume A3: x in dom f; let z be set; consider k being Element of product f; reconsider k as Function; defpred P[set] means $1 = x; deffunc F1(set) = z; deffunc F2(set) = k.$1; consider h being Function such that A4: dom h = dom f & for y being set st y in dom f holds (P[y] implies h.y = F1(y)) & (not P[y] implies h.y = F2(y)) from LambdaC; assume A5: z in f.x; now let y be set; assume y in dom f; then (y = x implies h.y = z) & (y <> x implies h.y = k.y) & k.y in f.y by A4,CARD_3:18; hence h.y in f.y by A5; end; then h in product f by A4,CARD_3:18; then h.x in g.x by A1,A2,A3,CARD_3:18; hence thesis by A3,A4; end; theorem Th2: for f,g being non-empty Function st product f = product g holds f = g proof let f,g be non-empty Function; assume A1: product f = product g; consider h being Element of product f; A2: (ex i being Function st h = i & dom i = dom g & for x being set st x in dom g holds i.x in g.x) & ex i being Function st h = i & dom i = dom f & for x being set st x in dom f holds i.x in f.x by A1,CARD_3:def 5; now let x be set; assume x in dom f; then f.x c= g.x & g.x c= f.x by A1,A2,Th1; hence f.x = g.x by XBOOLE_0:def 10; end; hence thesis by A2,FUNCT_1:9; end; definition let A be non empty set; let f be PFuncFinSequence of A; redefine func rng f -> Subset of PFuncs(A*, A); coherence by FINSEQ_1:def 4; end; definition let A,B be non empty set; let S be non empty Subset of PFuncs(A, B); redefine mode Element of S -> PartFunc of A,B; coherence proof let s be Element of S; thus thesis by PARTFUN1:120; 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 (the charact of A).o; correctness by FUNCT_1:def 5; end; begin :: Partitions definition let X be set; cluster -> with_non-empty_elements a_partition of X; coherence proof let P be a_partition of X; assume A1: {} in P; then X <> {} by EQREL_1:def 6; hence contradiction by A1,EQREL_1:def 6; end; end; definition let X be set; let R be Equivalence_Relation of X; redefine func Class R -> a_partition of X; coherence by EQREL_1:42; end; theorem Th3: for X being set, P being a_partition of X, x,a,b being set st x in a & a in P & x in b & b in P holds a = b proof let X be set, P be a_partition of X, x,a,b be set; assume A1: x in a & a in P & x in b & b in P; then X <> {} & a meets b by XBOOLE_0:3; hence thesis by A1,EQREL_1:def 6; end; theorem Th4: for X,Y being set st X is_finer_than Y for p being FinSequence of X ex q being FinSequence of Y st product p c= product q proof let X,Y be set; assume A1: for a being set st a in X ex b being set st b in Y & a c= b; let p be FinSequence of X; defpred P[set,set] means p.$1 c= $2; A2: for i being set st i in dom p ex y being set st y in Y & P[i,y] proof let i be set; assume i in dom p; then p.i in rng p & rng p c= X by FINSEQ_1:def 4,FUNCT_1:def 5; hence thesis by A1; 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 P[i,q.i] from NonUniqBoundFuncEx(A2); dom p = Seg len p by FINSEQ_1:def 3; then q is FinSequence by A3,FINSEQ_1:def 2; then q is FinSequence of Y & product p c= product q by A3,CARD_3:38,FINSEQ_1:def 4; hence thesis; end; theorem Th5: for X being set, 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 for p being FinSequence of P, q being FinSequence of Q holds product p c= product q iff f*p = q proof let X be set, P,Q be a_partition of X; let f be Function of P,Q such that A1: for a being set st a in P holds a c= f.a; let p be FinSequence of P, q be FinSequence of Q; A2: rng p c= P & rng q c= Q by FINSEQ_1:def 4; now assume P <> {}; then reconsider X as non empty set by EQREL_1:def 6; Q is a_partition of X; hence Q <> {}; end; then dom f = P & rng f c= Q by FUNCT_2:def 1,RELSET_1:12; then A3: dom (f*p) = dom p by A2,RELAT_1:46; hereby assume product p c= product q; then A4: dom p = dom q & for x being set st x in dom p holds p.x c= q.x by Th1; now let x be set; assume A5: x in dom p; then A6: p.x c= q.x & p.x in rng p & q.x in rng q by A4,FUNCT_1:def 5; then reconsider Y = X as non empty set by A2,EQREL_1:def 6; reconsider P' = P, Q' = Q as a_partition of Y; reconsider a = p.x as Element of P' by A2,A6; consider z being Element of a; a c= f.a & z in a & f is Function of P',Q' by A1; then z in f.a & z in q.x & f.a in Q' by A6,FUNCT_2:7; then q.x = f.a by A2,A6,Th3; hence (f*p).x = q.x by A5,FUNCT_1:23; end; hence f*p = q by A3,A4,FUNCT_1:9; end; assume A7: f*p = q; now let x be set; assume x in dom p; then q.x = f.(p.x) & p.x in rng p by A7,FUNCT_1:23,def 5; hence p.x c= q.x by A1,A2; end; hence product p c= product q by A3,A7,CARD_3:38; end; theorem Th6: for P being set, f being Function st rng f c= union P ex p being Function st dom p = dom f & rng p c= P & f in product p proof let P be set, f be Function; assume A1: rng f c= union P; defpred P[set,set] means f.$1 in $2; A2: for x being set st x in dom f ex a being set st a in P & P[x,a] proof let x be set; assume x in dom f; then f.x in rng f by FUNCT_1:def 5; then ex a being set st f.x in a & a in P by A1,TARSKI:def 4; hence thesis; 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 P[x,p.x] from NonUniqBoundFuncEx(A2); take p; thus thesis by A3,A4,CARD_3:def 5; end; theorem Th7: for X be set, P being a_partition of X, f being FinSequence of X ex p being FinSequence of P st f in product p proof let X be set, P be a_partition of X, f be FinSequence of X; X = {} or X <> {}; then rng f c= X & union P = X by EQREL_1:def 6,FINSEQ_1:def 4,ZFMISC_1:2; then consider p being Function such that A1: dom p = dom f & rng p c= P & f in product p by Th6; dom p = Seg len f by A1,FINSEQ_1:def 3; then p is FinSequence by FINSEQ_1:def 2; then p is FinSequence of P by A1,FINSEQ_1:def 4; hence thesis by A1; end; theorem for X,Y being non empty set for P being a_partition of X, Q being a_partition of Y holds {[:p,q:] where p is Element of P, q is Element of Q: not contradiction} is a_partition of [:X,Y:] proof let X,Y be non empty set; let P be a_partition of X, Q be a_partition of Y; set PQ = {[:p,q:] where p is Element of P, q is Element of Q: not contradiction}; PQ c= bool [:X,Y:] proof let x be set; assume x in PQ; then consider p being Element of P, q being Element of Q such that A1: x = [:p,q:]; thus thesis by A1; end; then reconsider PQ as Subset of bool [:X,Y:]; reconsider PQ as Subset-Family of [:X,Y:] by SETFAM_1:def 7; PQ is a_partition of [:X,Y:] proof per cases; case [:X,Y:] <> {}; thus union PQ c= [:X,Y:]; thus [:X,Y:] c= union PQ proof let x be set; assume x in [:X,Y:]; then consider x1,y1 being set such that A2: x1 in X & y1 in Y & x = [x1,y1] by ZFMISC_1:def 2; X = union P by EQREL_1:def 6; then consider p being set such that A3: x1 in p & p in P by A2,TARSKI:def 4; Y = union Q by EQREL_1:def 6; then consider q being set such that A4: y1 in q & q in Q by A2,TARSKI:def 4; x in [:p,q:] & [:p,q:] in PQ by A2,A3,A4,ZFMISC_1:106; hence thesis by TARSKI:def 4; end; let A be Subset of [:X,Y:]; assume A in PQ; then consider p being Element of P, q being Element of Q such that A5: A = [:p,q:]; thus A <> {} by A5; let B be Subset of [:X,Y:]; assume B in PQ; then consider p1 being Element of P, q1 being Element of Q such that A6: B = [:p1,q1:]; assume A <> B; then p <> p1 or q <> q1 by A5,A6; then p misses p1 or q misses q1 by EQREL_1:def 6; then p /\ p1 = {} or q /\ q1 = {} by XBOOLE_0:def 7; then A /\ B = [:{}, q /\ q1:] or A /\ B = [:p /\ p1,{}:] by A5,A6,ZFMISC_1:123 ; then A /\ B = {} by ZFMISC_1:113; hence A misses B by XBOOLE_0:def 7; case [:X,Y:] = {}; hence thesis; end; hence thesis; end; theorem Th9: for X being non empty set for P being a_partition of X holds {product p where p is Element of P*: not contradiction} is a_partition of X * proof let X be non empty set; let P be a_partition of X; set PP = {product p where p is Element of P*: not contradiction}; PP c= bool (X*) proof let x be set; assume x in PP; then consider p being Element of P* such that A1: x = product p; x c= X* proof let y be set; assume y in x; then consider f being Function such that A2: y = f & dom f = dom p & 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 A3: y is FinSequence by A2,FINSEQ_1:def 2; rng f c= X proof let z be set; assume z in rng f; then consider v being set such that A4: v in dom p & z = f.v by A2,FUNCT_1:def 5; p.v in rng p & rng p c= P by A4,FINSEQ_1:def 4,FUNCT_1:def 5; then p.v in P & P c= bool X; then z in p.v & p.v c= X by A2,A4; hence thesis; end; then y is FinSequence of X by A2,A3,FINSEQ_1:def 4; hence thesis by FINSEQ_1:def 11; end; hence thesis; end; then reconsider PP as Subset of bool (X*); reconsider PP as Subset-Family of (X*) by SETFAM_1:def 7; PP is a_partition of X* proof per cases; case X* <> {}; thus union PP c= X*; thus X* c= union PP proof let x be set; assume x in X*; then reconsider x as FinSequence of X by FINSEQ_1:def 11; rng x c= X & union P = X by EQREL_1:def 6,FINSEQ_1:def 4; then consider p being Function such that A5: dom p = dom x & rng p c= P & x in product p by Th6; dom p = Seg len x by A5,FINSEQ_1:def 3; then reconsider p as FinSequence by FINSEQ_1:def 2; reconsider p as FinSequence of P by A5,FINSEQ_1:def 4; reconsider p as Element of P* by FINSEQ_1:def 11; product p in PP; hence thesis by A5,TARSKI:def 4; end; let A be Subset of X*; assume A in PP; then consider p being Element of P* such that A6: A = product p; thus A <> {} by A6; let B be Subset of X*; assume B in PP; then consider q being Element of P* such that A7: B = product q; assume A8: A <> B; assume A meets B; then consider x being set such that A9: x in A & x in B by XBOOLE_0:3; consider f being Function such that A10: x = f & dom f = dom p & for z being set st z in dom p holds f.z in p.z by A6,A9,CARD_3:def 5; consider g being Function such that A11: x = g & dom g = dom q & for z being set st z in dom q holds g.z in q.z by A7,A9,CARD_3:def 5; now let z be set; assume z in dom p; then f.z in p.z & f.z in q.z & p.z in rng p & q.z in rng q & rng p c= P & rng q c= P by A10,A11,FINSEQ_1:def 4,FUNCT_1:def 5; then p.z meets q.z & p.z in P & q.z in P & P c= bool X by XBOOLE_0:3 ; hence p.z = q.z by EQREL_1:def 6; end; hence contradiction by A6,A7,A8,A10,A11,FUNCT_1:9; case X* = {}; hence thesis; end; hence thesis; end; theorem for X being non empty set, n be Nat for P being a_partition of X holds {product p where p is Element of n-tuples_on P: not contradiction} is a_partition of n-tuples_on X proof let X be non empty set, n be Nat; let P be a_partition of X; set nP = n-tuples_on P, nX = n-tuples_on X; set PP = {product p where p is Element of nP: not contradiction}; PP c= bool nX proof let x be set; assume x in PP; then consider p being Element of nP such that A1: x = product p; x c= nX proof let y be set; assume y in x; then consider f being Function such that A2: y = f & dom f = dom p & for z being set st z in dom p holds f.z in p.z by A1,CARD_3:def 5; A3: dom p = Seg len p by FINSEQ_1:def 3; then reconsider y as FinSequence by A2,FINSEQ_1:def 2; rng f c= X proof let z be set; assume z in rng f; then consider v being set such that A4: v in dom p & z = f.v by A2,FUNCT_1:def 5; p.v in rng p & rng p c= P by A4,FINSEQ_1:def 4,FUNCT_1:def 5; then p.v in P & P c= bool X; then z in p.v & p.v c= X by A2,A4; hence thesis; end; then y is FinSequence of X & len y = len p & len p = n by A2,A3,FINSEQ_1:def 3,def 4,FINSEQ_2:109; then y is Element of nX by FINSEQ_2:110; hence thesis; end; hence thesis; end; then reconsider PP as Subset of bool (nX); reconsider PP as Subset-Family of nX by SETFAM_1:def 7; PP is a_partition of nX proof per cases; case nX <> {}; thus union PP c= nX; thus nX c= union PP proof let x be set; assume x in nX; then reconsider x as Element of nX; rng x c= X & union P = X by EQREL_1:def 6,FINSEQ_1:def 4; then consider p being Function such that A5: dom p = dom x & rng p c= P & x in product p by Th6; A6: dom p = Seg len x by A5,FINSEQ_1:def 3; then reconsider p as FinSequence by FINSEQ_1:def 2; reconsider p as FinSequence of P by A5,FINSEQ_1:def 4; len p = len x & len x = n by A6,FINSEQ_1:def 3,FINSEQ_2:109; then reconsider p as Element of nP by FINSEQ_2:110; product p in PP; hence thesis by A5,TARSKI:def 4; end; let A be Subset of nX; assume A in PP; then consider p being Element of nP such that A7: A = product p; thus A <> {} by A7; let B be Subset of nX; assume B in PP; then consider q being Element of nP such that A8: B = product q; assume A9: A <> B; assume A meets B; then consider x being set such that A10: x in A & x in B by XBOOLE_0:3; consider f being Function such that A11: x = f & dom f = dom p & for z being set st z in dom p holds f.z in p.z by A7,A10,CARD_3:def 5; consider g being Function such that A12: x = g & dom g = dom q & for z being set st z in dom q holds g.z in q.z by A8,A10,CARD_3:def 5; now let z be set; assume z in dom p; then f.z in p.z & f.z in q.z & p.z in rng p & q.z in rng q & rng p c= P & rng q c= P by A11,A12,FINSEQ_1:def 4,FUNCT_1:def 5; then p.z meets q.z & p.z in P & q.z in P & P c= bool X by XBOOLE_0:3 ; hence p.z = q.z by EQREL_1:def 6; end; hence contradiction by A7,A8,A9,A11,A12,FUNCT_1:9; case nX = {}; hence thesis; end; hence thesis; end; theorem Th11: for X being non empty set, Y be set st Y c= X 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, Y be set; assume A1: Y c= X; let P be a_partition of X; set Q = {a /\ Y where a is Element of P: a meets Y}; Q c= bool Y proof let x be set; assume x in Q; then consider p being Element of P such that A2: x = p /\ Y & p meets Y; x c= X /\ Y & X /\ Y = Y by A1,A2,XBOOLE_1:26,28; hence thesis; end; then reconsider Q as Subset-Family of Y by SETFAM_1:def 7; Q is a_partition of Y proof per cases; case Y <> {}; thus union Q c= Y; thus Y c= union Q proof let x be set; assume A3: x in Y; then x in X & X = union P by A1,EQREL_1:def 6; then consider p being set such that A4: x in p & p in P by TARSKI:def 4; p meets Y by A3,A4,XBOOLE_0:3; then x in p /\ Y & p /\ Y in Q by A3,A4,XBOOLE_0:def 3; hence thesis by TARSKI:def 4; end; let A be Subset of Y; assume A in Q; then consider p being Element of P such that A5: A = p /\ Y & p meets Y; thus A <> {} by A5,XBOOLE_0:def 7; let B be Subset of Y; assume B in Q; then consider p1 being Element of P such that A6: B = p1 /\ Y & p1 meets Y; assume A <> B; then p misses p1 by A5,A6,EQREL_1:def 6; then A misses p1 by A5,XBOOLE_1:74; hence A misses B by A6,XBOOLE_1:74; case A7: Y = {}; assume Q <> {}; then reconsider Q as non empty set; consider q being Element of Q; q in Q; then ex a being Element of P st q = a /\ Y & a meets Y; hence contradiction by A7,XBOOLE_1:65; end; hence thesis; end; theorem Th12: for f being non empty Function, P being a_partition of dom f holds {f|a where a is Element of P: not contradiction} is a_partition of f proof let f be non empty Function; set X = dom f; let P be a_partition of X; set Y = f; set Q = {f|a where a is Element of P: not contradiction}; Q c= bool Y proof let x be set; assume x in Q; then consider p being Element of P such that A1: x = f|p; x c= f by A1,RELAT_1:88; hence thesis; end; then reconsider Q as Subset-Family of Y by SETFAM_1:def 7; Q is a_partition of Y proof per cases; case Y <> {}; thus union Q c= Y; thus Y c= union Q proof let x be set; assume A2: x in f; then consider y,z being set such that A3: x = [y,z] by RELAT_1:def 1; y in X & X = union P by A2,A3,EQREL_1:def 6,RELAT_1:def 4; then consider p being set such that A4: y in p & p in P by TARSKI:def 4; x in f|p & f|p in Q by A2,A3,A4,RELAT_1:def 11; hence thesis by TARSKI:def 4; end; let A be Subset of Y; assume A in Q; then consider p being Element of P such that A5: A = f|p; reconsider p as non empty Subset of X; consider x being Element of p; [x,f.x] in f by FUNCT_1:def 4; hence A <> {} by A5,RELAT_1:def 11; let B be Subset of Y; assume B in Q; then consider p1 being Element of P such that A6: B = f|p1; assume A <> B; then A7: p misses p1 by A5,A6,EQREL_1:def 6; assume A meets B; then consider x being set such that A8: x in A & x in B by XBOOLE_0:3; consider y,z being set such that A9: x = [y,z] by A8,RELAT_1:def 1; y in p & y in p1 by A5,A6,A8,A9,RELAT_1:def 11; hence contradiction by A7,XBOOLE_0:3; case Y = {}; hence thesis; end; hence thesis; end; definition let X be set; func SmallestPartition X -> a_partition of X equals :Def2: Class id X; correctness; end; theorem Th13: for X being non empty set holds SmallestPartition X = {{x} where x is Element of X: not contradiction} proof let X be non empty set; set Y = {{x} where x is Element of X: not contradiction}; A1: SmallestPartition X = Class id X by Def2; hereby let x be set; assume x in SmallestPartition X; then consider y being set such that A2: y in X & x = Class(id X, y) by A1,EQREL_1:def 5; x = {y} by A2,EQREL_1:33; hence x in Y by A2; end; let x be set; assume x in Y; then consider y being Element of X such that A3: x = {y}; Class(id X, y) = x by A3,EQREL_1:33; hence thesis by A1,EQREL_1:def 5; end; theorem Th14: for X being set, p being FinSequence of SmallestPartition X ex q being FinSequence of X st product p = {q} proof let X be set; set P = SmallestPartition X; let p be FinSequence of P; consider q being Element of product p; A1: dom q = dom p by CARD_3:18; then reconsider q as FinSequence by Lm1; A2: q in product p & product p c= Funcs(dom p, Union p) by FUNCT_6:10; then A3: q in Funcs(dom p, Union p) & rng p c= P & Union p = union rng p by FINSEQ_1:def 4,PROB_1:def 3; ex f being Function st q = f & dom f = dom p & rng f c= Union p by A2,FUNCT_2:def 2; then rng q c= Union p & Union p c= union P by A3,ZFMISC_1:95; then rng q c= union P & (X = {} or X <> {}) by XBOOLE_1:1; then rng q c= X by EQREL_1:def 6,ZFMISC_1:2; then reconsider q as FinSequence of X by FINSEQ_1:def 4; take q; thus product p c= {q} proof let x be set; assume x in product p; then consider g being Function such that A4: x = g & dom g = dom p and A5: for x being set st x in dom p holds g.x in p.x by CARD_3:def 5; now let y be set; assume y in dom p; then A6: g.y in p.y & q.y in p.y & p.y in rng p by A5,CARD_3:18,FUNCT_1: def 5; then A7: p.y in P by A3; reconsider X as non empty set by A3,A6,EQREL_1:def 6; P = {{z} where z is Element of X: not contradiction} by Th13; then consider z being Element of X such that A8: p.y = {z} by A7; thus g.y = z by A6,A8,TARSKI:def 1 .= q.y by A6,A8,TARSKI:def 1; end; then x = q by A1,A4,FUNCT_1:9; hence thesis by TARSKI:def 1; end; thus thesis by ZFMISC_1:37; end; definition let X be set; mode IndexedPartition of X -> Function means: Def3: rng it is a_partition of X & it is one-to-one; existence proof consider p being a_partition of X; take id p; thus thesis by FUNCT_1:52,RELAT_1:71; end; end; definition let X be set; cluster -> one-to-one non-empty IndexedPartition of X; coherence proof let P be IndexedPartition of X; thus P is one-to-one by Def3; let x be set; assume x in dom P; then P.x in rng P & rng P is a_partition of X & (X = {} or X <> {}) by Def3,FUNCT_1:def 5; hence thesis by EQREL_1:def 6; end; let P be IndexedPartition of X; redefine func rng P -> a_partition of X; coherence by Def3; end; definition let X be non empty set; cluster -> non empty IndexedPartition of X; coherence proof let P be IndexedPartition of X; consider a being Element of rng P; ex b being set st [b,a] in P by RELAT_1:def 5; hence thesis; end; end; definition let X be set, P be a_partition of X; redefine func id P -> IndexedPartition of X; coherence proof rng id P = P & id P is one-to-one by FUNCT_1:52,RELAT_1:71; hence thesis by Def3; end; end; definition let X be set; let P be IndexedPartition of X; let x be set; assume A1: x in X; then A2: union rng P = X by EQREL_1:def 6; func P-index_of x -> set means: Def4: it in dom P & x in P.it; existence proof consider a being set such that A3: x in a & a in rng P by A1,A2,TARSKI:def 4; ex y being set st y in dom P & a = P.y by A3,FUNCT_1:def 5; hence thesis by A3; end; correctness proof let y1,y2 be set; assume A4: y1 in dom P & x in P.y1 & y2 in dom P & x in P.y2; then P.y1 in rng P & P.y2 in rng P & P.y1 meets P.y2 by FUNCT_1:def 5,XBOOLE_0:3; then P.y1 = P.y2 by A1,EQREL_1:def 6; hence y1 = y2 by A4,FUNCT_1:def 8; end; end; theorem Th15: for X being set, 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, P be non-empty Function such 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; rng P c= bool X proof let y be set; assume y in rng P; then y c= union rng P by ZFMISC_1:92; then y c= X by A1,PROB_1:def 3; hence thesis; end; then reconsider Y = rng P as Subset-Family of X by SETFAM_1:def 7; Y is a_partition of X proof per cases; case X <> {}; thus union Y = X by A1,PROB_1:def 3; let A be Subset of X; assume A in Y; then A3: ex x being set st x in dom P & A = P.x by FUNCT_1:def 5; hence A<>{} by UNIALG_1:def 6; let B be Subset of X; assume B in Y; then ex y being set st y in dom P & B = P.y by FUNCT_1:def 5; hence A = B or A misses B by A2,A3; case A4: X = {}; assume Y <> {}; then reconsider Y as non empty set; consider y being Element of Y; ex x being set st x in dom P & y = P.x by FUNCT_1:def 5; then reconsider y as non empty set by UNIALG_1:def 6; consider x being Element of y; x in union rng P by TARSKI:def 4; hence contradiction by A1,A4,PROB_1:def 3; end; hence rng P is a_partition of X; let x,y be set; assume A5: x in dom P & y in dom P & P.x = P.y & x <> y; then reconsider Px = P.x, Py = P.y as non empty set by UNIALG_1:def 6; consider a being Element of Px; P.x misses P.y by A2,A5; then not a in Py by XBOOLE_0:3; hence contradiction by A5; end; theorem Th16: for X,Y being non empty set, 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, P be a_partition of Y; let f be Function of X, P; assume A1: P c= rng f; rng f c= P by RELSET_1:12; then rng f = P by A1,XBOOLE_0:def 10; hence thesis by Def3; end; begin :: Relations generated by operations of partial algebra scheme IndRelationEx {A, B() -> non empty set, i() -> Nat, R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}: ex R being Relation of A(),B(), F being ManySortedSet of NAT st R = F.i() & F.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F.i holds F.(i+1) = RR(R,i) proof deffunc G(set,set) = RR($2,$1); consider F being Function such that A1: dom F = NAT and A2: F.0 = R0() & for n being Nat holds F.(n+1) = G(n,F.n) from LambdaRecEx; reconsider F as ManySortedSet of NAT by A1,PBOOLE:def 3; defpred P[Nat] means F.$1 is Relation of A(),B(); A3: P[0] by A2; A4: now let i be Nat; assume P[i]; then reconsider R = F.i as Relation of A(),B(); F.(i+1) = RR(R,i) by A2; hence P[i+1]; end; for i being Nat holds P[i] from Ind(A3,A4); then reconsider R = F.i() as Relation of A(),B(); take R,F; thus thesis by A2; end; scheme RelationUniq {A, B() -> non empty set, P[set,set]}: for R1, R2 being Relation of A(), B() st (for x being Element of A(), y being Element of B() holds [x,y] in R1 iff P[x,y]) & (for x being Element of A(), y being Element of B() holds [x,y] in R2 iff P[x,y]) holds R1 = R2 proof let R1, R2 be Relation of A(), B() such that A1: for x being Element of A(), y being Element of B() holds [x,y] in R1 iff P[x,y] and A2: for x being Element of A(), y being Element of B() holds [x,y] in R2 iff P[x,y]; let x,y be set; hereby assume A3: [x,y] in R1; then reconsider a = x as Element of A() by ZFMISC_1:106; reconsider b = y as Element of B() by A3,ZFMISC_1:106; P[a,b] by A1,A3; hence [x,y] in R2 by A2; end; assume A4: [x,y] in R2; then reconsider a = x as Element of A() by ZFMISC_1:106; reconsider b = y as Element of B() by A4,ZFMISC_1:106; P[a,b] by A2,A4; hence thesis by A1; end; scheme IndRelationUniq {A, B() -> non empty set, i() -> Nat, R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}: for R1, R2 being Relation of A(),B() st (ex F being ManySortedSet of NAT st R1 = F.i() & F.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F.i holds F.(i+1) = RR(R,i)) & (ex F being ManySortedSet of NAT st R2 = F.i() & F.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F.i holds F.(i+1) = RR(R,i)) holds R1 = R2 proof let R1, R2 be Relation of A(),B(); given F1 being ManySortedSet of NAT such that A1: R1 = F1.i() & F1.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F1.i holds F1.(i+1) = RR(R,i); given F2 being ManySortedSet of NAT such that A2: R2 = F2.i() & F2.0 = R0() & for i being Nat, R being Relation of A(),B() st R = F2.i holds F2.(i+1) = RR(R,i); defpred P[Nat] means F1.$1 = F2.$1 & F1.$1 is Relation of A(),B(); A3: P[0] by A1,A2; A4: now let i be Nat; assume A5: P[i]; then reconsider R = F1.i as Relation of A(),B(); F1.(i+1) = RR(R,i) & F2.(i+1) = RR(R,i) by A1,A2,A5; hence P[i+1]; end; for i being Nat holds P[i] from Ind(A3,A4); hence thesis by A1,A2; end; definition let A be partial non-empty UAStr; func DomRel A -> Relation of the carrier of A means :Def5: for x,y being Element of A holds [x,y] in it iff for f being operation of A, p,q being FinSequence holds p^<*x*>^q in dom f iff p^<*y*>^q in dom f; existence proof defpred P[set,set] means for f be operation of A, p,q be FinSequence holds p^<*$1*>^q in dom f iff p^<*$2*>^q in dom f; thus ex D be Relation of the carrier of A st for x,y being Element of A holds [x,y] in D iff P[x,y] from Rel_On_Dom_Ex; end; uniqueness proof defpred P[set,set] means for f be operation of A, p,q be FinSequence holds p^<*$1*>^q in dom f iff p^<*$2*>^q in dom f; thus for D1,D2 be Relation of the carrier of A st (for x,y being Element of A holds [x,y] in D1 iff P[x,y]) & (for x,y being Element of A holds [x,y] in D2 iff P[x,y]) holds D1 = D2 from RelationUniq; end; end; definition let A be partial non-empty UAStr; cluster DomRel A -> total symmetric transitive; coherence proof set X = the carrier of A; DomRel A is_reflexive_in X proof let x be set; for f being operation of A for a,b be FinSequence holds a^<*x*>^b in dom f iff a^<*x*>^b in dom f; hence thesis by Def5; end; then A1: dom DomRel A = X & field DomRel A = X by ORDERS_1:98; hence DomRel A is total by PARTFUN1:def 4; DomRel A is_symmetric_in X proof let x,y be set; assume x in X & y in X; then reconsider x' = x, y' = y as Element of X; assume [x,y] in DomRel A; then for f being operation of A for a,b be FinSequence holds a^<*x'*>^b in dom f iff a^<*y'*>^b in dom f by Def5; hence thesis by Def5; end; hence DomRel A is symmetric by A1,RELAT_2:def 11; DomRel A is_transitive_in X proof let x,y,z be set; assume x in X & y in X & z in X; then reconsider x' = x, y' = y, z' = z as Element of X; assume A2: [x,y] in DomRel A & [y,z] in DomRel A; now let f be operation of A, a,b be FinSequence; a^<*x'*>^b in dom f iff a^<*y'*>^b in dom f by A2,Def5; hence a^<*x'*>^b in dom f iff a^<*z'*>^b in dom f by A2,Def5; end; hence thesis by Def5; end; hence DomRel A is transitive by A1,RELAT_2:def 16; end; end; definition let A be non-empty partial UAStr; let R be Relation of the carrier of A; func R|^A -> Relation of the carrier of A means: Def6: 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 proof defpred P[set,set] means [$1,$2] in R & for f be operation of A for p,q be 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 be Relation of the carrier of A st for x,y being Element of A holds [x,y] in D iff P[x,y] from Rel_On_Dom_Ex; end; uniqueness proof defpred P[set,set] means [$1,$2] in R & for f be operation of A for p,q be 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 be Relation of the carrier of A st (for x,y being Element of A holds [x,y] in D1 iff P[x,y]) & (for x,y being Element of A holds [x,y] in D2 iff P[x,y]) holds D1 = D2 from RelationUniq; end; end; definition let A be non-empty partial UAStr; let R be Relation of the carrier of A; let i be Nat; func R|^(A,i) -> Relation of the carrier of A means: Def7: ex F being ManySortedSet of NAT st it = F.i & F.0 = R & for i being Nat, R being Relation of the carrier of A st R = F.i holds F.(i+1) = R|^A; existence proof deffunc RR(Relation of the carrier of A,the carrier of A,Nat) = $1 |^ A; thus ex D be Relation of the carrier of A st ex F being ManySortedSet of NAT st D = F.i & F.0 = R & for i being Nat, R being Relation of the carrier of A st R = F.i holds F.(i+1) = RR(R,i) from IndRelationEx; end; uniqueness proof deffunc RR(Relation of the carrier of A,the carrier of A,Nat) = $1 |^ A; thus for D1,D2 be Relation of the carrier of A st (ex F being ManySortedSet of NAT st D1 = F.i & F.0 = R & for i being Nat, R being Relation of the carrier of A st R = F.i holds F.(i+1) = RR(R,i)) & (ex F being ManySortedSet of NAT st D2 = F.i & F.0 = R & for i being Nat, R being Relation of the carrier of A st R = F.i holds F.(i+1) = RR(R,i)) holds D1 = D2 from IndRelationUniq; end; end; theorem Th17: for A being non-empty partial UAStr, R being Relation of the carrier of A holds R|^(A,0) = R & R|^(A,1) = R|^A proof let A be non-empty partial UAStr; let R be Relation of the carrier of A; consider F being ManySortedSet of NAT such that R|^(A,0) = F.0 and A1: F.0 = R & for i being Nat, R being Relation of the carrier of A st R = F.i holds F.(i+1) = R|^A by Def7; F.(0+1) = R|^A by A1; hence thesis by A1,Def7; end; theorem Th18: for A being non-empty partial UAStr, i being Nat, R being Relation of the carrier of A holds R|^(A,i+1) = R|^(A,i)|^A proof let A be non-empty partial UAStr; let i be Nat; let R be Relation of the carrier of A; consider F being ManySortedSet of NAT such that A1: R|^(A,i) = F.i and A2: F.0 = R & for i being Nat, R being Relation of the carrier of A st R = F.i holds F.(i+1) = R|^A by Def7; F.(i+1) = R|^(A,i)|^A by A1,A2; hence thesis by A2,Def7; end; theorem for A being non-empty partial UAStr, i,j being Nat, R being Relation of the carrier of A holds R|^(A,i+j) = R|^(A,i)|^(A,j) proof let A be non-empty partial UAStr; let i,j be Nat; let R be Relation of the carrier of A; defpred P[Nat] means R|^(A,i+$1) = R|^(A,i)|^(A,$1); A1: P[0] by Th17; A2: now let j be Nat; assume A3: P[j]; R|^(A,i+(j+1)) = R|^(A,(i+j)+1) by XCMPLX_1:1 .= R|^(A,i+j)|^A by Th18 .= R|^(A,i)|^(A,j+1) by A3,Th18; hence P[j+1]; end; for j being Nat holds P[j] from Ind(A1,A2); hence thesis; end; theorem Th20: for A being non-empty partial UAStr for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds R|^A is total symmetric transitive proof let A be non-empty partial UAStr; let R be Equivalence_Relation of the carrier of A; assume A1: R c= DomRel A; now let x be set; assume x in the carrier of A; then reconsider a = x as Element of A; A2: [a,a] in R by EQREL_1:11; now let f be operation of A, p,q be FinSequence; assume p^<*a*>^q in dom f & p^<*a*>^q in dom f; then f.(p^<*a*>^q) in rng f & f.(p^<*a*>^q) in rng f & rng f c= the carrier of A by FUNCT_1:def 5,RELSET_1:12; hence [f.(p^<*a*>^q), f.(p^<*a*>^q)] in R by EQREL_1:11; end; hence [x,x] in R|^A by A2,Def6; end; then R|^A is_reflexive_in the carrier of A by RELAT_2:def 1; then A3: dom(R|^A) = the carrier of A & field(R|^A) = the carrier of A by ORDERS_1:98; hence R|^A is total by PARTFUN1:def 4; now let x,y be set; assume x in the carrier of A & y in the carrier of A; then reconsider a = x, b = y as Element of A; assume A4: [x,y] in R|^A; then A5: [a,b] in R & for f being operation of A for p,q being FinSequence st p^<*a*>^q in dom f & p^<*b*>^q in dom f holds [f.(p^<*a*>^q), f.(p^<*b*>^q)] in R by Def6; now thus [b,a] in R by A5,EQREL_1:12; let f be operation of A; let p,q be FinSequence; assume p^<*b*>^q in dom f & p^<*a*>^q in dom f; then [f.(p^<*a*>^q), f.(p^<*b*>^q)] in R by A4,Def6; hence [f.(p^<*b*>^q), f.(p^<*a*>^q)] in R by EQREL_1:12; end; hence [y,x] in R|^A by Def6; end; then R|^A is_symmetric_in the carrier of A by RELAT_2:def 3; hence R|^A is symmetric by A3,RELAT_2:def 11; now let x,y,z be set; assume x in the carrier of A & y in the carrier of A & z in the carrier of A; then reconsider a = x, b = y, c = z as Element of A; assume A6: [x,y] in R|^A & [y,z] in R|^A; A7: now let f be operation of A; let p,q be FinSequence; [a,b] in R by A6,Def6; then (p^<*a*>^q in dom f iff p^<*b*>^q in dom f) & (p^<*a*>^q in dom f & p^<*b*>^q in dom f implies [f.(p^<*a*>^q), f.(p^<*b*>^q)] in R) & (p^<*b*>^q in dom f & p^<*c*>^q in dom f implies [f.(p^<*b*>^q), f.(p^<*c*>^q)] in R) by A1,A6,Def5,Def6; 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 EQREL_1:13; end; [a,b] in R & [b,c] in R by A6,Def6; then [a,c] in R by EQREL_1:13; hence [x,z] in R|^A by A7,Def6; end; then R|^A is_transitive_in the carrier of A by RELAT_2:def 8; hence R|^A is transitive by A3,RELAT_2:def 16; end; theorem Th21: for A being non-empty partial UAStr for R being Relation of the carrier of A holds R|^A c= R proof let A be non-empty partial UAStr; let R be Relation of the carrier of A; let x,y be set; assume A1: [x,y] in R|^A; then x in the carrier of A & y in the carrier of A by ZFMISC_1:106; hence [x,y] in R by A1,Def6; end; theorem Th22: for A being non-empty partial UAStr for R being Equivalence_Relation of the carrier of A st R c= DomRel A for i being Nat holds R|^(A,i) is total symmetric transitive proof let A be non-empty partial UAStr; let R be Equivalence_Relation of the carrier of A such that A1: R c= DomRel A; defpred P[Nat] means R|^(A,$1) c= DomRel A & R|^(A,$1) is total symmetric transitive; A2: P[0] by A1,Th17; A3: now let i be Nat; assume A4: P[i]; R|^(A,i)|^A c= R|^(A,i) & R|^(A,i)|^A = R|^(A,i+1) by Th18,Th21; hence P[i+1] by A4,Th20,XBOOLE_1:1; end; for i being Nat holds P[i] from Ind(A2,A3); hence thesis; end; definition let A be non-empty partial UAStr; func LimDomRel A -> Relation of the carrier of A means: Def8: for x,y being Element of A holds [x,y] in it iff for i being Nat holds [x,y] in (DomRel A)|^(A,i); existence proof defpred P[set,set] means for i being Nat holds [$1,$2] in (DomRel A)|^(A,i); thus ex D be Relation of the carrier of A st for x,y being Element of A holds [x,y] in D iff P[x,y] from Rel_On_Dom_Ex; end; uniqueness proof defpred P[set,set] means for i being Nat holds [$1,$2] in (DomRel A)|^(A,i); thus for D1,D2 be Relation of the carrier of A st (for x,y being Element of A holds [x,y] in D1 iff P[x,y]) & (for x,y being Element of A holds [x,y] in D2 iff P[x,y]) holds D1 = D2 from RelationUniq; end; end; theorem Th23: for A being non-empty partial UAStr holds LimDomRel A c= DomRel A proof let A be non-empty partial UAStr, x,y be set; assume A1: [x,y] in LimDomRel A; then x in the carrier of A & y in the carrier of A by ZFMISC_1:106; then [x,y] in (DomRel A)|^(A,0) by A1,Def8; hence thesis by Th17; end; definition let A be non-empty partial UAStr; cluster LimDomRel A -> total symmetric transitive; coherence proof now let x be set; assume x in the carrier of A; then reconsider a = x as Element of A; now let i be Nat; BB: (DomRel A)|^(A,i) is total symmetric transitive by Th22; then (DomRel A)|^(A,i) is reflexive by RELAT_2:22; hence [a,a] in (DomRel A)|^(A,i) by BB,EQREL_1:11; end; hence [x,x] in LimDomRel A by Def8; end; then LimDomRel A is_reflexive_in the carrier of A by RELAT_2:def 1; then A1: dom(LimDomRel A) = the carrier of A & field(LimDomRel A) = the carrier of A by ORDERS_1:98; hence LimDomRel A is total by PARTFUN1:def 4; now let x,y be set; assume x in the carrier of A & y in the carrier of A; then reconsider a = x, b = y as Element of A; assume A2: [x,y] in LimDomRel A; now let i be Nat; (DomRel A)|^(A,i) is total symmetric transitive & [a,b] in (DomRel A)|^(A,i) by A2,Def8,Th22; hence [b,a] in (DomRel A)|^(A,i) by EQREL_1:12; end; hence [y,x] in LimDomRel A by Def8; end; then LimDomRel A is_symmetric_in the carrier of A by RELAT_2:def 3; hence LimDomRel A is symmetric by A1,RELAT_2:def 11; now let x,y,z be set; assume x in the carrier of A & y in the carrier of A & z in the carrier of A; then reconsider a = x, b = y, c = z as Element of A; assume A3: [x,y] in LimDomRel A & [y,z] in LimDomRel A; now let i be Nat; (DomRel A)|^(A,i) is total symmetric transitive & [a,b] in (DomRel A)|^(A,i) & [b,c] in (DomRel A)|^(A,i) by A3,Def8,Th22; hence [a,c] in (DomRel A)|^(A,i) by EQREL_1:13; end; hence [x,z] in LimDomRel A by Def8; end; then LimDomRel A is_transitive_in the carrier of A by RELAT_2:def 8; hence LimDomRel A is transitive by A1,RELAT_2:def 16; end; end; begin :: Partitability definition let X be non empty set; let f be PartFunc of X*, X; let P be a_partition of X; pred f is_partitable_wrt P means: Def9: for p being FinSequence of P ex a being Element of P st f.:product p c= a; end; definition let X be non empty set; let f be PartFunc of X*, X; let P be a_partition of X; pred f is_exactly_partitable_wrt P means: Def10: f is_partitable_wrt P & for p being FinSequence of P st product p meets dom f holds product p c= dom f; end; theorem for A being non-empty partial UAStr for f being operation of A holds f is_exactly_partitable_wrt SmallestPartition the carrier of A proof let A be non-empty partial UAStr; set P = SmallestPartition the carrier of A; let f be operation of A; hereby let p be FinSequence of P; consider q being FinSequence of the carrier of A such that A1: product p = {q} by Th14; 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 5,RELSET_1:12; then consider x being Element of A such that A2: q in dom f & x = f.q or not q in dom f; P = {{z} where z is Element of A: not contradiction} by Th13; then {x} in P; then reconsider a = {x} as Element of P; take a; thus f.:product p c= a proof let z be set; assume z in f.:product p; then consider y being set such that A3: y in dom f & y in product p & z = f.y by FUNCT_1:def 12; y = q by A1,A3,TARSKI:def 1; hence z in a by A2,A3,TARSKI:def 1; end; end; let p be FinSequence of P; consider q being FinSequence of the carrier of A such that A4: product p = {q} by Th14; assume product p meets dom f; then consider x being set such that A5: x in product p & x in dom f by XBOOLE_0:3; let z be set; assume z in product p; then z = q & x = q by A4,A5,TARSKI:def 1; hence z in dom f by A5; end; scheme FiniteTransitivity {x, y() -> FinSequence, P[set], R[set,set]}: P[y()] provided A1: P[x()] and A2: len x() = len y() and A3: for p,q being FinSequence, z1,z2 being set st P[p^<*z1*>^q] & R[z1,z2] holds P[p^<*z2*>^q] and A4: for i being Nat st i in dom x() holds R[x().i, y().i] proof defpred Q[Nat] means for x1,x2, y1,y2 being FinSequence st len x1 = $1 & x() = x1^x2 & len y1 = $1 & y() = y1^y2 holds P[y1^x2]; A5: Q[0] proof let x1,x2, y1,y2 be FinSequence; assume A6: len x1 = 0 & x() = x1^x2 & len y1 = 0 & y() = y1^y2; then x1 = {} & y1 = {} by FINSEQ_1:25; hence P[y1^x2] by A1,A6; end; A7: for i being Nat st Q[i] holds Q[i+1] proof let i be Nat such that A8: for x1,x2, y1,y2 being FinSequence st len x1 = i & x() = x1^x2 & len y1 = i & y() = y1^y2 holds P[y1^x2]; let x1,x2, y1,y2 be FinSequence such that A9: len x1 = i+1 & x() = x1^x2 & len y1 = i+1 & y() = y1^y2; A10: x1 <> {} & y1 <> {} by A9,FINSEQ_1:25; then consider x' being FinSequence, xx being set such that A11: x1 = x'^<*xx*> by FINSEQ_1:63; consider y' being FinSequence, yy being set such that A12: y1 = y'^<*yy*> by A10,FINSEQ_1:63; A13: dom x1 = Seg len x1 & dom y1 = Seg len y1 by FINSEQ_1:def 3; len <*xx*> = 1 & len <*yy*> = 1 by FINSEQ_1:57; then len x1 = len x'+1 & len y1 = len y'+1 by A11,A12,FINSEQ_1:35; then len x' = i & x() = x'^(<*xx*>^x2) & len y' = i & y() = y'^(<*yy*>^ y2) & i+1 in dom x1 & dom x1 c= dom x() & x1.(len x'+1) = xx & y1.(len y'+1) = yy by A9,A11,A12,A13,FINSEQ_1:6,39,45,59,XCMPLX_1:2; then P[y'^(<*xx*>^x2)] & i+1 in dom x() & x().(i+1) = xx & y().(i+1) = yy by A8,A9,A13,FINSEQ_1:def 7; then P[y'^<*xx*>^x2] & R[xx,yy] by A4,FINSEQ_1:45; hence thesis by A3,A12; end; A14: for i being Nat holds Q[i] from Ind(A5,A7); x() = x()^{} & y() = y()^{} by FINSEQ_1:47; hence thesis by A2,A14; end; theorem Th25: for A being non-empty partial UAStr for f being operation of A holds f is_exactly_partitable_wrt Class LimDomRel A proof let A be non-empty partial UAStr; set P = Class LimDomRel A; let f be operation of A; hereby let p be FinSequence of P; consider a0 being Element of P; per cases; suppose product p meets dom f; then consider x being set such that A1: x in product p & x in dom f by XBOOLE_0:3; A2: f.x in the carrier of A by A1,PARTFUN1:27; then reconsider a = Class(LimDomRel A, f.x) as Element of P by EQREL_1:def 5; take a; thus f.:product p c= a proof let y be set; assume y in f.:product p; then consider z being set such that A3: z in dom f & z in product p & y = f.z by FUNCT_1:def 12; product p c= Funcs(dom p, Union p) by FUNCT_6:10; then A4: (ex f being Function st x = f & dom f = dom p & rng f c= Union p) & (ex f being Function st z = f & dom f = dom p & rng f c= Union p) by A1,A3,FUNCT_2:def 2; then reconsider x, z as Function; A5: dom p = Seg len p by FINSEQ_1:def 3; then reconsider x, z as FinSequence by A4,FINSEQ_1:def 2; defpred P[set] means $1 in dom f & f.$1 in a; defpred R[set,set] means [$1,$2] in LimDomRel A; len x = len p & len z = len p by A4,A5,FINSEQ_1:def 3; then A6: len x = len z; A7: P[x] by A1,A2,EQREL_1:28; A8: for p1,q1 being FinSequence, z1,z2 being set st P[p1^<*z1*>^q1] & R[z1,z2] holds P[p1^<*z2*>^q1] proof let p1,q1 be FinSequence, z1,z2 be set; assume A9: p1^<*z1*>^q1 in dom f & f.(p1^<*z1*>^q1) in a & [z1,z2] in LimDomRel A; then A10: [f.(p1^<*z1*>^q1), f.x] in LimDomRel A by EQREL_1:27; LimDomRel A c= DomRel A by Th23; then A11: z1 in the carrier of A & z2 in the carrier of A & [z1,z2] in DomRel A by A9,ZFMISC_1:106; hence A12: p1^<*z2*>^q1 in dom f by A9,Def5; then A13: f.(p1^<*z1*>^q1) in rng f & f.(p1^<*z2*>^q1) in rng f & rng f c= the carrier of A by A9,FUNCT_1:def 5,RELSET_1:12; now let i be Nat; [z1,z2] in (DomRel A)|^(A,i+1) by A9,A11,Def8; then [z1,z2] in (DomRel A)|^(A,i)|^A by Th18; then [f.(p1^<*z1*>^q1),f.(p1^<*z2*>^q1)] in (DomRel A)|^(A,i) & (DomRel A)|^(A,i) is total symmetric transitive by A9,A11,A12,Def6,Th22; hence [f.(p1^<*z2*>^q1),f.(p1^<*z1*>^q1)] in (DomRel A)|^(A,i) by EQREL_1:12; end; then [f.(p1^<*z2*>^q1),f.(p1^<*z1*>^q1)] in LimDomRel A by A13,Def8; then [f.(p1^<*z2*>^q1), f.x] in LimDomRel A by A10,EQREL_1:13; hence thesis by EQREL_1:27; end; A14: for i being Nat st i in dom x holds R[x.i, z.i] proof let i be Nat; assume A15: i in dom x; then p.i in rng p & rng p c= P by A4,FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider a = p.i as Element of P; (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) & (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 A1,A3,CARD_3:def 5; then (ex b being set st b in the carrier of A & a = Class(LimDomRel A, b)) & x.i in a & z.i in a by A15,EQREL_1:def 5; hence [x.i, z.i] in LimDomRel A by EQREL_1:30; end; P[z] from FiniteTransitivity(A7,A6,A8,A14); hence thesis by A3; end; suppose product p misses dom f; then (product p) /\ dom f = {} by XBOOLE_0:def 7; then f.:product p = f.:{} by RELAT_1:145 .= {} by RELAT_1:149; then f.:product p c= a0 by XBOOLE_1:2; hence ex a being Element of P st f.:product p c= a; end; let p be FinSequence of P; assume product p meets dom f; then consider x being set such that A16: x in product p & x in dom f by XBOOLE_0:3; let y be set; assume A17: y in product p; product p c= Funcs(dom p, Union p) by FUNCT_6:10; then A18: (ex f being Function st x = f & dom f = dom p & rng f c= Union p) & (ex f being Function st y = f & dom f = dom p & rng f c= Union p) by A16,A17,FUNCT_2:def 2; then reconsider x, z = y as Function; A19: dom p = Seg len p by FINSEQ_1:def 3; then reconsider x, z as FinSequence by A18,FINSEQ_1:def 2; defpred P[set] means $1 in dom f; defpred R[set,set] means [$1,$2] in LimDomRel A; len x = len p & len z = len p by A18,A19,FINSEQ_1:def 3; then A20: len x = len z; A21: P[x] by A16; A22: for p1,q1 being FinSequence, z1,z2 being set st P[p1^<*z1*>^q1] & R[z1,z2] holds P[p1^<*z2*>^q1] proof let p1,q1 be FinSequence, z1,z2 be set; assume A23: p1^<*z1*>^q1 in dom f & [z1,z2] in LimDomRel A; LimDomRel A c= DomRel A by Th23; then z1 in the carrier of A & z2 in the carrier of A & [z1,z2] in DomRel A by A23,ZFMISC_1:106; hence p1^<*z2*>^q1 in dom f by A23,Def5; end; A24: for i being Nat st i in dom x holds R[x.i, z.i] proof let i be Nat; assume A25: i in dom x; then p.i in rng p & rng p c= P by A18,FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider a = p.i as Element of P; (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) & (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 A16,A17,CARD_3:def 5; then (ex b being set st b in the carrier of A & a = Class(LimDomRel A, b)) & x.i in a & z.i in a by A25,EQREL_1:def 5; hence [x.i, z.i] in LimDomRel A by EQREL_1:30; end; P[z] from FiniteTransitivity(A21,A20,A22,A24); hence y in dom f; end; definition let A be partial non-empty UAStr; mode a_partition of A -> a_partition of the carrier of A means: Def11: for f being operation of A holds f is_exactly_partitable_wrt it; existence proof for f being operation of A holds f is_exactly_partitable_wrt Class LimDomRel A by Th25; hence thesis; end; end; definition let A be partial non-empty UAStr; mode IndexedPartition of A -> IndexedPartition of the carrier of A means: Def12: rng it is a_partition of A; existence proof consider P being a_partition of A; take id P; thus thesis by RELAT_1:71; end; end; definition let A be partial non-empty UAStr; let P be IndexedPartition of A; redefine func rng P -> a_partition of A; coherence by Def12; end; theorem for A being non-empty partial UAStr holds Class LimDomRel A is a_partition of A proof let A be partial non-empty UAStr; thus for f being operation of A holds f is_exactly_partitable_wrt Class LimDomRel A by Th25; end; theorem Th27: for X being non empty set, P being a_partition of X for p being FinSequence of P, q1,q2 being FinSequence, 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, P be a_partition of X; let pp be FinSequence of P; let p,q be FinSequence; let x,y be set; assume A1: p^<*x*>^q in product pp; given a being Element of P such that A2: x in a & y in a; reconsider x,y as Element of a by A2; now A3: 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:35 .= Seg ((len p+len <*y*>)+len q) by FINSEQ_1:35 .= Seg ((len p+1)+len q) by FINSEQ_1:57 .= Seg ((len p+len <*x*>)+len q) by FINSEQ_1:57 .= Seg (len (p^<*x*>)+len q) by FINSEQ_1:35 .= Seg len (p^<*x*>^q) by FINSEQ_1:35 .= dom pp by A3,FINSEQ_1:def 3; let i be set; assume A4: i in dom pp; then reconsider ii = i as Nat; A5: len <*x*> = 1 & len <*y*> = 1 & dom <*x*> = Seg 1 & dom <*y*> = Seg 1 by FINSEQ_1:55,57; then A6: len (p^<*x*>) = len p+1 & len (p^<*y*>) = len p+1 by FINSEQ_1:35; then A7: dom (p^<*x*>) = Seg (len p+1) & dom (p^<*y*>) = Seg (len p+1) by FINSEQ_1:def 3; A8: ii in dom (p^<*x*>) or ex n being Nat st n in dom q & ii = len (p^<*x*>)+n by A3,A4,FINSEQ_1:38; A9: dom p c= dom (p^<*y*>) & dom (p^<*y*>) c= dom (p^<*y*>^q) by FINSEQ_1:39; per cases by A8,FINSEQ_1:38; suppose ii in dom p; then (p^<*y*>).i = p.i & (p^<*x*>).i = p.i & ii in dom (p^<*y*>) by A9,FINSEQ_1:def 7; then (p^<*y*>^q).i = p.i & (p^<*x*>^q).i = p.i by A7,FINSEQ_1:def 7; hence (p^<*y*>^q).i in pp.i by A3,A4; suppose (ex n being Nat st n in dom <*x*> & ii = len p+n); then consider n being Nat such that A10: n in Seg 1 & ii = len p+n by A5; n = 1 by A10,FINSEQ_1:4,TARSKI:def 1; then (p^<*x*>).ii = x & (p^<*y*>).ii = y & ii in dom (p^<*y*>) by A7,A10,FINSEQ_1:6,59; then A11: (p^<*x*>^q).ii = x & (p^<*y*>^q).ii = y by A7,FINSEQ_1:def 7; then x in pp.i & pp.i in rng pp & rng pp c= P by A3,A4,FINSEQ_1:def 4,FUNCT_1:def 5; then pp.i in P & a meets pp.i by XBOOLE_0:3; then pp.i = a by EQREL_1:def 6; hence (p^<*y*>^q).i in pp.i by A11; suppose ex n being Nat st n in dom q & ii = len (p^<*x*>)+n; then consider n being Nat such that A12: n in dom q & ii = len (p^<*x*>)+n; (p^<*y*>^q).i = q.n & (p^<*x*>^q).i = q.n by A6,A12,FINSEQ_1:def 7; hence (p^<*y*>^q).i in pp.i by A3,A4; end; hence thesis by CARD_3:def 5; end; theorem Th28: for A being partial non-empty UAStr, P being a_partition of A holds P is_finer_than Class LimDomRel A proof let A be partial non-empty UAStr; let P be a_partition of A; consider EP being Equivalence_Relation of the carrier of A such that A1: P = Class EP by EQREL_1:43; let a be set; assume a in P; then reconsider aa = a as Element of P; consider x being Element of aa; take Class(LimDomRel A, x); thus Class(LimDomRel A, x) in Class LimDomRel A by EQREL_1:def 5; let y be set; assume y in a; then reconsider y as Element of aa; reconsider x,y as Element of A; defpred P[Nat] means EP c= (DomRel A)|^(A,$1); A2: P[0] proof let x,y be set; assume A3: [x,y] in EP; then reconsider x,y as Element of A by ZFMISC_1:106; reconsider a = Class(EP, y) as Element of P by A1,EQREL_1:def 5; A4: x in a & y in a by A3,EQREL_1:27,28; for f being operation of A, 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, p,q be FinSequence; A5: f is_exactly_partitable_wrt P by Def11; now let p,q be FinSequence, x,y be Element of a; assume A6: p^<*x*>^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 A7: p^<*x*>^q in product pp by Th7; product pp meets dom f by A6,A7,XBOOLE_0:3; then A8: product pp c= dom f by A5,Def10; p^<*y*>^q in product pp by A7,Th27; hence p^<*y*>^q in dom f by A8; end; hence p^<*x*>^q in dom f iff p^<*y*>^q in dom f by A4; end; then [x,y] in DomRel A by Def5; hence thesis by Th17; end; A9: for i being Nat st P[i] holds P[i+1] proof let i be Nat; assume A10: EP c= (DomRel A)|^(A,i); let x,y be set; assume A11: [x,y] in EP; then reconsider x,y as Element of A by ZFMISC_1:106; reconsider a = Class(EP, y) as Element of P by A1,EQREL_1:def 5; now let f be operation of A, p,q be FinSequence; assume A12: p^<*x*>^q in dom f & 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 A13: p^<*x*>^q in product pp by Th7; f is_exactly_partitable_wrt P by Def11; then f is_partitable_wrt P by Def10; then consider c being Element of P such that A14: f.:product pp c= c by Def9; x in a & y in a by A11,EQREL_1:27,28; then p^<*y*>^q in product pp by A13,Th27; then f.(p^<*x*>^q) in f.:product pp & f.(p^<*y*>^q) in f.:product pp by A12,A13,FUNCT_1:def 12; then f.(p^<*x*>^q) in c & f.(p^<*y*>^q) in c & ex x being set st x in the carrier of A & c = Class(EP,x) by A1,A14,EQREL_1:def 5; then [f.(p^<*x*>^q), f.(p^<*y*>^q)] in EP by EQREL_1:30; hence [f.(p^<*x*>^q), f.(p^<*y*>^q)] in (DomRel A)|^(A,i) by A10; end; then [x,y] in (DomRel A)|^(A,i)|^A by A10,A11,Def6; hence thesis by Th18; end; A15: for i being Nat holds P[i] from Ind(A2,A9); now let i be Nat; ex x being set st x in the carrier of A & aa = Class(EP, x) by A1,EQREL_1:def 5; then [x,y] in EP & EP c= (DomRel A)|^(A,i) by A15,EQREL_1:30; hence [x,y] in (DomRel A)|^(A,i); end; then [x,y] in LimDomRel A by Def8; then [y,x] in LimDomRel A by EQREL_1:12; hence thesis by EQREL_1:27; end; begin :: Morphisms between manysorted signatures definition let S1,S2 be ManySortedSign; let f,g be Function; pred f,g form_morphism_between S1,S2 means: Def13: dom f = the carrier of S1 & dom g = the OperSymbols of S1 & rng f c= the carrier of S2 & rng g c= the OperSymbols of S2 & f*the ResultSort of S1 = (the ResultSort of S2)*g & for o being set, p being Function st o in the OperSymbols of S1 & p = (the Arity of S1).o holds f*p = (the Arity of S2).(g.o); end; theorem Th29: for S being non void non empty ManySortedSign holds id the carrier of S, id the OperSymbols of S form_morphism_between S,S proof let S be non void non empty ManySortedSign; set f = id the carrier of S, g = id the OperSymbols of S; A1: dom the ResultSort of S = the OperSymbols of S & rng the ResultSort of S c= the carrier of S & dom the Arity of S = the OperSymbols of S by FUNCT_2:def 1,RELSET_1:12; then f*the ResultSort of S = the ResultSort of S by RELAT_1:79; hence dom f = the carrier of S & dom g = the OperSymbols of S & rng f c= the carrier of S & rng g c= the OperSymbols of S & f*the ResultSort of S = (the ResultSort of S)*g by A1,FUNCT_1:42,RELAT_1:71 ; let o be set, p be Function; assume A2: o in the OperSymbols of S & p = (the Arity of S).o; then A3: g.o = o & p in (the carrier of S)* by FUNCT_1:34,FUNCT_2:7; 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 f*p = (the Arity of S).(g.o) by A2,A3,RELAT_1:79; end; theorem Th30: 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; let f1,f2, g1,g2 be Function such that A1: dom f1 = the carrier of S1 & dom g1 = the OperSymbols of S1 and A2: rng f1 c= the carrier of S2 & rng g1 c= the OperSymbols of S2 and A3: f1*the ResultSort of S1 = (the ResultSort of S2)*g1 and A4: for o being set, p being Function st o in the OperSymbols of S1 & p = (the Arity of S1).o holds f1*p = (the Arity of S2).(g1.o) and A5: dom f2 = the carrier of S2 & dom g2 = the OperSymbols of S2 and A6: rng f2 c= the carrier of S3 & rng g2 c= the OperSymbols of S3 and A7: f2*the ResultSort of S2 = (the ResultSort of S3)*g2 and A8: for o being set, p being Function st o in the OperSymbols of S2 & p = (the Arity of S2).o holds f2*p = (the Arity of S3).(g2.o); set f = f2*f1, g = g2*g1; thus dom f = the carrier of S1 & dom g = the OperSymbols of S1 by A1,A2,A5,RELAT_1:46; rng f c= rng f2 & rng g c= rng g2 by RELAT_1:45; hence rng f c= the carrier of S3 & rng g c= the OperSymbols of S3 by A6,XBOOLE_1:1; thus f*the ResultSort of S1 = f2*((the ResultSort of S2)*g1) by A3,RELAT_1:55 .= f2*(the ResultSort of S2)*g1 by RELAT_1:55 .= (the ResultSort of S3)*g by A7,RELAT_1:55; let o be set, p be Function; assume A9: o in the OperSymbols of S1 & p = (the Arity of S1).o; then A10: f1*p = (the Arity of S2).(g1.o) & g1.o in rng g1 by A1,A4,FUNCT_1:def 5; f*p = f2*(f1*p) & g.o = g2.(g1.o) by A1,A9,FUNCT_1:23,RELAT_1:55; hence f*p = (the Arity of S3).(g.o) by A2,A8,A10; end; definition let S1,S2 be ManySortedSign; pred S1 is_rougher_than S2 means ex f,g being Function st f,g form_morphism_between S2,S1 & rng f = the carrier of S1 & rng g = the OperSymbols of S1; end; definition let S1,S2 be non void non empty ManySortedSign; redefine pred S1 is_rougher_than S2; reflexivity proof let S be non void non empty ManySortedSign; take f = id the carrier of S, g = id the OperSymbols of S; thus f,g form_morphism_between S,S & rng f = the carrier of S & rng g = the OperSymbols of S by Th29,RELAT_1:71; end; end; theorem 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; given f1,g1 being Function such that A1: f1,g1 form_morphism_between S2,S1 & rng f1 = the carrier of S1 & rng g1 = the OperSymbols of S1; given f2,g2 being Function such that A2: f2,g2 form_morphism_between S3,S2 & rng f2 = the carrier of S2 & rng g2 = the OperSymbols of S2; take f = f1*f2, g = g1*g2; thus f,g form_morphism_between S3,S1 by A1,A2,Th30; dom f1 = the carrier of S2 & dom g1 = the OperSymbols of S2 by A1,Def13; hence rng f = the carrier of S1 & rng g = the OperSymbols of S1 by A1,A2,RELAT_1:47; end; begin :: Manysorted signature of partital algebra definition let A be partial non-empty UAStr; let P be a_partition of A; func MSSign(A,P) -> strict ManySortedSign means: Def15: the carrier of it = P & the OperSymbols 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, 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 proof set O = {[f,p] where f is OperSymbol of A, p is Element of P*: product p meets dom Den(f, A)}; defpred Q[set,set] means ex f being OperSymbol of A, q being Element of P* st q = $2 & $1 = [f,q]; A1: for o being set st o in O ex p being set st p in P* & Q[o,p] proof let o be set; assume o in O; then consider f being OperSymbol of A, p being Element of P* such that A2: o = [f,p] & product p meets dom Den(f,A); take p; thus thesis by A2; end; defpred S[set,set] means ex f being OperSymbol of A, p being Element of P* st $1 = [f,p] & Den(f,A).:product p c= $2; A3: for o being set st o in O ex r being set st r in P & S[o,r] proof let o be set; assume o in O; then consider f being OperSymbol of A, p being Element of P* such that A4: o = [f,p] & product p meets dom Den(f,A); Den(f,A) is_exactly_partitable_wrt P by Def11; then Den(f,A) is_partitable_wrt P by Def10; then ex a being Element of P st Den(f,A).:product p c= a by Def9; hence thesis by A4; end; consider Ar being Function such that A5: dom Ar = O & rng Ar c= P* and A6: for o being set st o in O holds Q[o,Ar.o] from NonUniqBoundFuncEx(A1); reconsider Ar as Function of O, P* by A5,FUNCT_2:4; consider R being Function such that A7: dom R = O & rng R c= P and A8: for o being set st o in O holds S[o,R.o] from NonUniqBoundFuncEx(A3); reconsider R as Function of O, P by A7,FUNCT_2:4; take S = ManySortedSign(#P, O, Ar, R#); thus the carrier of S = P & the OperSymbols of S = O; let f be OperSymbol of A, p be Element of P*; set o = [f, p]; assume product p meets dom Den(f, A); then A9: o in O; then consider f1 being OperSymbol of A, q1 being Element of P* such that A10: q1 = Ar.o & o = [f1,q1] by A6; consider f2 being OperSymbol of A, q2 being Element of P* such that A11: o = [f2,q2] & Den(f2,A).:product q2 c= R.o by A8,A9; q1 = p & q2 = p & f2 = f by A10,A11,ZFMISC_1:33; hence thesis by A10,A11; end; correctness 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 such that A12: the carrier of S1 = P and A13: the OperSymbols of S1 = O and A14: for f being OperSymbol of A, 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 A15: the carrier of S2 = P and A16: the OperSymbols of S2 = O and A17: for f being OperSymbol of A, 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]; A18: dom the Arity of S1 = O & dom the Arity of S2 = O by A13,A16,FUNCT_2:def 1; now let o be set; assume o in O; then consider f being OperSymbol of A, p being Element of P* such that A19: o = [f,p] & product p meets dom Den(f,A); thus (the Arity of S1).o = p by A14,A19 .= (the Arity of S2).o by A17,A19 ; end; then A20: the Arity of S1 = the Arity of S2 by A18,FUNCT_1:9; A21: dom the ResultSort of S1 = O & dom the ResultSort of S2 = O by A12,A13,A15,A16,FUNCT_2:def 1; consider R being Equivalence_Relation of the carrier of A such that A22: P = Class R by EQREL_1:43; now let o be set; assume A23: o in O; then consider f being OperSymbol of A, p being Element of P* such that A24: o = [f,p] & product p meets dom Den(f,A); consider x being set such that A25: x in product p & x in dom Den(f,A) by A24,XBOOLE_0:3; Den(f,A).x in Den(f,A).:product p & Den(f,A).:product p c= (the ResultSort of S1).o & Den(f,A).:product p c= (the ResultSort of S2).o & (the ResultSort of S1).o in P & (the ResultSort of S2).o in P by A12,A13,A14,A15,A16,A17,A23,A24,A25,FUNCT_1:def 12,FUNCT_2:7; then Den(f,A).x in (the ResultSort of S1).o & Den(f,A).x in (the ResultSort of S2).o & (ex y being set st y in the carrier of A & (the ResultSort of S1).o = Class(R,y)) & (ex y being set st y in the carrier of A & (the ResultSort of S2).o = Class(R,y)) by A22,EQREL_1:def 5; then (the ResultSort of S1).o = Class(R,Den(f,A).x) & (the ResultSort of S2).o = Class(R,Den(f,A).x) by EQREL_1:31; hence (the ResultSort of S1).o = (the ResultSort of S2).o; end; hence thesis by A12,A13,A15,A16,A20,A21,FUNCT_1:9; end; end; definition let A be partial non-empty UAStr; let P be a_partition of A; cluster MSSign(A,P) -> non empty non void; coherence proof thus the carrier of MSSign(A,P) is non empty by Def15; consider g being OperSymbol of A; consider x being Element of dom Den(g,A); reconsider x as Element of (the carrier of A)*; union P = the carrier of A & rng x c= the carrier of A by EQREL_1:def 6,FINSEQ_1:def 4; then consider q being Function such that A1: dom q = dom x & rng q c= P & x in product q by Th6; dom x = Seg len x by FINSEQ_1:def 3; then reconsider q as FinSequence by A1,FINSEQ_1:def 2; reconsider q as FinSequence of P by A1,FINSEQ_1:def 4; reconsider q as Element of P* by FINSEQ_1:def 11; product q meets dom Den(g, A) & the OperSymbols 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 A1,Def15,XBOOLE_0:3; then [g,q] in the OperSymbols of MSSign(A,P); hence the OperSymbols of MSSign(A,P) <> {}; 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); redefine func o`1 -> OperSymbol of A; coherence proof o in the OperSymbols of MSSign(A,P) & the OperSymbols 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 Def15; then ex f being OperSymbol of A, p being Element of P* st o = [f,p] & product p meets dom Den(f, A); hence thesis by MCART_1:7; end; func o`2 -> Element of P*; coherence proof o in the OperSymbols of MSSign(A,P) & the OperSymbols 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 Def15; then ex f being OperSymbol of A, p being Element of P* st o = [f,p] & product p meets dom Den(f,A); hence thesis by MCART_1:7; end; end; definition let A be partial non-empty UAStr; let S be non void non empty ManySortedSign; let G be MSAlgebra over S; let P be IndexedPartition of the OperSymbols of S; pred A can_be_characterized_by S,G,P means: Def16: 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; definition let A be partial non-empty UAStr; let S be non void non empty ManySortedSign; pred A can_be_characterized_by S means ex G being MSAlgebra over S, P being IndexedPartition of the OperSymbols of S st A can_be_characterized_by S,G,P; end; theorem for A being partial non-empty UAStr, P being a_partition of A holds A can_be_characterized_by MSSign(A, P) proof let A be partial non-empty UAStr; let P be a_partition of A; set S = MSSign(A, P); dom id P = P & P = the carrier of S by Def15,RELAT_1:71; then reconsider Z = id P as ManySortedSet of the carrier of S by PBOOLE:def 3; deffunc F1(OperSymbol of S) = Den($1`1, A)|product $1`2; consider D being ManySortedSet of the OperSymbols of S such that A1: for o being OperSymbol of S holds D.o = F1(o) from LambdaDMS; deffunc F2(OperSymbol of A) = {a where a is OperSymbol of S: 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 = F2(o) from LambdaDMS; A3: dom Q = dom the charact of A by PBOOLE:def 3; A4: the carrier of S = P & the OperSymbols of S = {[o,p] where o is OperSymbol of A, p is Element of P*: product p meets dom Den(o,A)} by Def15; Q is non-empty proof let x be set; assume x in dom Q; then reconsider o = x as OperSymbol of A by PBOOLE:def 3; consider y being Element of dom Den(o,A); reconsider y as Element of (the carrier of A)*; rng y c= the carrier of A & the carrier of A = union P by EQREL_1:def 6,FINSEQ_1:def 4; then consider f being Function such that A5: dom f = dom y & rng f c= P & y in product f by Th6; dom y = Seg len y by FINSEQ_1:def 3; then f is FinSequence by A5,FINSEQ_1:def 2; then f is FinSequence of P by A5,FINSEQ_1:def 4; then reconsider f as Element of P* by FINSEQ_1:def 11; product f meets dom Den(o,A) by A5,XBOOLE_0:3; then [o,f] in the OperSymbols of S & [o,f]`1 = o & Q.o = {a where a is OperSymbol of S: a`1 = o} by A2,A4,MCART_1:7; then [o,f] in Q.x; hence Q.x is not empty; end; then reconsider Q as non-empty Function; D is ManySortedFunction of Z# * the Arity of S, Z * the ResultSort of S proof let x be set; assume A6: x in the OperSymbols of S; then consider o being OperSymbol of A, p being Element of P* such that A7: x = [o,p] & product p meets dom Den(o,A) by A4; reconsider xx = x as OperSymbol of S by A6; A8: rng the ResultSort of S c= the carrier of S & dom the Arity of S = the OperSymbols of S by FUNCT_2:def 1,RELSET_1:12; rng p c= P by FINSEQ_1:def 4; then (the Arity of S).x = p & (Z# ).p = product(Z*p) & Z*p = p by A4,A7,Def15,MSUALG_1:def 3,RELAT_1:79; then A9: (Z# * the Arity of S).x = product p by A6,A8,FUNCT_1:23; A10: Den(o, A).:product p c= (the ResultSort of S).x & xx`2 = p & xx`1 = o by A7,Def15,MCART_1:7; then A11: rng (Den(o, A)|product p) = Den(o, A).:product p & D.xx = Den(o, A)|product p by A1,RELAT_1:148; Den(o,A) is_exactly_partitable_wrt P by Def11; then product p c= dom Den(o,A) by A7,Def10; then Z * the ResultSort of S = the ResultSort of S & dom (Den(o, A)|product p) = product p by A4,A8,RELAT_1:79,91; hence thesis by A9,A10,A11,FUNCT_2:4; end; then reconsider D as ManySortedFunction of Z# * the Arity of S, Z * the ResultSort of S; A12: Union Q = the OperSymbols of S proof hereby let x be set; assume x in Union Q; then consider y being set such that A13: y in dom Q & x in Q.y by CARD_5:10; reconsider y as OperSymbol of A by A13,PBOOLE:def 3; Q.y = {a where a is OperSymbol of S: a`1 = y} by A2; then ex a being OperSymbol of S st x = a & a`1 = y by A13; hence x in the OperSymbols of S; end; let x be set; assume x in the OperSymbols of S; then reconsider b = x as OperSymbol of S; Q.b`1 = {a where a is OperSymbol of S: a`1 = b`1} by A2; then b in Q.b`1; hence thesis by A3,CARD_5:10; end; now let x,y be set; assume A14: x in dom Q & y in dom Q & x <> y; then reconsider a = x, b = y as OperSymbol of A by PBOOLE:def 3; thus Q.x misses Q.y proof assume Q.x meets Q.y; then consider z being set such that A15: z in Q.x & z in Q.y by XBOOLE_0:3; Q.a = {c where c is OperSymbol of S: c`1 = a} & Q.b = {c where c is OperSymbol of S: c`1 = b} by A2; then (ex c1 being OperSymbol of S st z = c1 & c1`1 = a) & (ex c2 being OperSymbol of S st z = c2 & c2`1 = b) by A15; hence contradiction by A14; end; end; then reconsider Q as IndexedPartition of the OperSymbols of S by A12,Th15; take G = MSAlgebra(#Z, D#), Q; id P is IndexedPartition of A proof thus rng id P is a_partition of A by RELAT_1:71; end; hence the Sorts of G is IndexedPartition of A; thus dom Q = dom the charact of A by PBOOLE:def 3; let o be OperSymbol of A; reconsider PP = {product p where p is Element of P*: not contradiction} 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); A16: Q.o in rng Q & rng Q c= bool the OperSymbols of S by A3,FUNCT_1:def 5 ; then Q.o c= the OperSymbols of S & dom D = the OperSymbols of S by PBOOLE:def 3; then A17: dom F = Q.o & Q.o <> {} & dom {} = {} by A16,EQREL_1:def 6,RELAT_1: 91; then reconsider F as non empty Function; reconsider Qo = Q.o as non empty set by A16,EQREL_1:def 6; reconsider RR = {Den(o,A)|a where a is Element of QQ: not contradiction} as a_partition of Den(o,A) by Th12; A18: Q.o = {a where a is OperSymbol of S: a`1 = o} by A2; rng F c= RR proof let y be set; assume y in rng F; then consider x be set such that A19: x in dom F & y = F.x by FUNCT_1:def 5; x in dom (the Charact of G) /\ (Q.o) by A19,RELAT_1:90; then x in Q.o by XBOOLE_0:def 3; then consider a being OperSymbol of S such that A20: x = a & a`1 = o by A18; a in the OperSymbols of S; then consider s being OperSymbol of A, p being Element of P* such that A21: a = [s,p] & product p meets dom Den(s,A) by A4; A22: s = o & a`2 = p & product p in PP & Den(o,A) is_exactly_partitable_wrt P by A20,A21,Def11,MCART_1:7; then (product p) /\ dom Den(o,A) in QQ & product p c= dom Den(o,A) by A21,Def10; then product p in QQ by XBOOLE_1:28; then Den(o,A)|product p in RR & y = D.a by A19,A20,FUNCT_1:70; hence thesis by A1,A20,A22; end; then reconsider F as Function of Qo, RR by A17,FUNCT_2:4; A23: RR c= rng F proof let x be set; assume x in RR; then consider a being Element of QQ such that A24: x = Den(o,A)|a; a in QQ; then consider b being Element of PP such that A25: a = b /\ dom Den(o,A) & b meets dom Den(o,A); b in PP; then consider p being Element of P* such that A26: b = product p; Den(o,A) is_exactly_partitable_wrt P by Def11; then product p c= dom Den(o,A) by A25,A26,Def10; then A27: b = a by A25,A26,XBOOLE_1:28; [o,p] in the OperSymbols of S & [o,p]`1 = o & [o,p]`2 = p by A4,A25,A26,MCART_1:7; then [o,p] in dom D & [o,p] in Q.o & D.[o,p] = x by A1,A18,A24,A26,A27,PBOOLE:def 3; hence thesis by FUNCT_1:73; end; F is one-to-one proof let x1,x2 be set; assume A28: x1 in dom F & x2 in dom F & F.x1 = F.x2; then consider a1 being OperSymbol of S such that A29: x1 = a1 & a1`1 = o by A17,A18; consider a2 being OperSymbol of S such that A30: x2 = a2 & a2`1 = o by A17,A18,A28; a1 in the OperSymbols of S; then consider o1 being OperSymbol of A, p1 being Element of P* such that A31: a1 = [o1,p1] & product p1 meets dom Den(o1,A) by A4; a2 in the OperSymbols of S; then consider o2 being OperSymbol of A, p2 being Element of P* such that A32: a2 = [o2,p2] & product p2 meets dom Den(o2,A) by A4; F.x1 = D.a1 & F.x1 = D.a2 & a1`2 = p1 & a2`2 = p2 by A28,A29,A30,A31,A32,FUNCT_1:70,MCART_1:7; then A33: F.x1 = Den(o,A)|product p1 & F.x1 = Den(o,A)|product p2 by A1,A29, A30; A34: Den(o,A) is_exactly_partitable_wrt P & o = o1 & o = o2 by A29,A30,A31,A32,Def11,MCART_1:7; then product p1 c= dom Den(o,A) & product p2 c= dom Den(o,A) by A31,A32,Def10; then product p1 = dom (Den(o,A)|product p1) & product p2 = dom (Den(o,A)|product p2) by RELAT_1:91; hence thesis by A29,A30,A31,A32,A33,A34,Th2; end; hence thesis by A23,Th16; end; theorem Th33: for A being partial non-empty UAStr for S being non void non empty ManySortedSign for G being MSAlgebra over S for Q being IndexedPartition of the OperSymbols of S st A can_be_characterized_by S,G,Q for o being OperSymbol of A, r being FinSequence of rng the Sorts of G st product r c= dom Den(o,A) 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; let S2 be non void non empty ManySortedSign; let G be MSAlgebra over S2, Q be IndexedPartition of the OperSymbols of S2 such that A1: the Sorts of G is IndexedPartition of A & dom Q = dom the charact of A and A2: for o being OperSymbol of A holds (the Charact of G)|(Q.o) is IndexedPartition of Den(o, A); reconsider R = the Sorts of G as IndexedPartition of A by A1; dom R = the carrier of S2 by PBOOLE:def 3; then reconsider SG = the Sorts of G as Function of the carrier of S2, rng R by FUNCT_2:def 1,RELSET_1:11; let o be OperSymbol of A, r be FinSequence of rng the Sorts of G; reconsider p = r as Element of (rng R)* by FINSEQ_1:def 11; assume A3: product r c= dom Den(o,A); reconsider P = (the Charact of G)|(Q.o) as IndexedPartition of Den(o, A) by A2; consider h being Element of product p; h in product r; then [h,Den(o,A).h] in Den(o, A) by A3,FUNCT_1:def 4; then A4: P-index_of [h,Den(o,A).h] in dom P & [h,Den(o,A).h] in P.(P-index_of [h,Den(o,A).h]) by Def4; reconsider Qo = Q.o as Element of rng Q by A1,FUNCT_1:def 5; A5: dom the Charact of G = the OperSymbols of S2 by PBOOLE:def 3; then A6: dom P = Qo by RELAT_1:91; reconsider s = P-index_of [h,Den(o,A).h] as Element of Qo by A4,A5,RELAT_1: 91; reconsider q = SG*the_arity_of s as FinSequence of rng R by Lm2; reconsider q as Element of (rng R)* by FINSEQ_1:def 11; reconsider Q = {product t where t is Element of (rng R)* : not contradiction} as a_partition of (the carrier of A)* by Th9; take s; A7: dom the Arity of S2 = the OperSymbols of S2 by FUNCT_2:def 1; A8: Args(s,G) = ((the Sorts of G)# * the Arity of S2).s by MSUALG_1:def 9 .= (the Sorts of G)# .((the Arity of S2).s) by A7,FUNCT_1:23 .= (the Sorts of G)# .the_arity_of s by MSUALG_1:def 6 .= product q by MSUALG_1:def 3; A9: product q in Q & product p in Q; P.s = (the Charact of G).s by A6,FUNCT_1:70; then P.s = Den(s,G) by MSUALG_1:def 11; then h in dom Den(s,G) by A4,RELAT_1:def 4; then product p = product q by A8,A9,Th3; hence (the Sorts of G)*the_arity_of s = r by Th2; thus thesis; end; theorem for A being partial non-empty UAStr, P being a_partition of A st P = Class LimDomRel A for S being non void non empty ManySortedSign st A can_be_characterized_by S holds MSSign(A,P) is_rougher_than S proof let A be partial non-empty UAStr, P be a_partition of A; assume A1: P = Class LimDomRel A; set S1 = MSSign(A,P); let S2 be non void non empty ManySortedSign; given G being MSAlgebra over S2, Q being IndexedPartition of the OperSymbols of S2 such that A2: A can_be_characterized_by S2,G,Q; A3: the Sorts of G is IndexedPartition of A & dom Q = dom the charact of A by A2,Def16; then reconsider G as non-empty MSAlgebra over S2 by MSUALG_1:def 8; reconsider R = the Sorts of G as IndexedPartition of A by A2,Def16; A4: dom R = the carrier of S2 by PBOOLE:def 3; then reconsider SG = the Sorts of G as Function of the carrier of S2, rng R by FUNCT_2:def 1,RELSET_1:11; A5: the OperSymbols of S1 = {[o,p] where o is OperSymbol of A, p is Element of P*: product p meets dom Den(o,A)} by Def15; A6: the carrier of S1 = P by Def15; defpred Q[set,set] means $1 c= $2; A7: rng R is_finer_than P by A1,Th28; then A8: for r being set st r in rng R ex p being set st p in P & Q[r,p] by SETFAM_1:def 2; consider em being Function such that A9: dom em = rng R & rng em c= P and A10: for r being set st r in rng R holds Q[r,em.r] from NonUniqBoundFuncEx(A8); reconsider em as Function of rng R, P by A9,FUNCT_2:4; dom (em*R) = dom R & rng (em*R) = rng em by A9,RELAT_1:46,47; then reconsider f = em*R as Function of the carrier of S2, the carrier of S1 by A4,A6,A9,FUNCT_2:4; take f; defpred S[set,set] means ex p being FinSequence of P, o being OperSymbol of S2 st $2 = [Q-index_of $1, p] & $1 = o & Args(o,G) c= product p; A11: for s2 being set st s2 in the OperSymbols of S2 ex s1 being set st s1 in the OperSymbols of S1 & S[s2,s1] proof let s2 be set; assume s2 in the OperSymbols of S2; then reconsider 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 A12: product (SG*the_arity_of s2) c= product p by A7,Th4; reconsider p as Element of P* by FINSEQ_1:def 11; take s1 = [Q-index_of s2, p]; reconsider o = Q-index_of s2 as OperSymbol of A by A3,Def4; consider aa being Element of Args(s2,G); A13: aa in Args(s2,G); A14: dom Den(s2,G) = Args(s2,G) by FUNCT_2:def 1; A15: dom the Arity of S2 = the OperSymbols of S2 & dom the Charact of G = the OperSymbols of S2 by FUNCT_2:def 1,PBOOLE:def 3; (the Charact of G)|(Q.o) is IndexedPartition of Den(o, A) by A2,Def16; then rng ((the Charact of G)|(Q.o)) is a_partition of Den(o, A) by Def3; then (the Charact of G).:(Q.o) is a_partition of Den(o, A) & s2 in Q.o by Def4,RELAT_1:148; then Den(s2, G) = (the Charact of G).s2 & (the Charact of G).s2 in (the Charact of G).:(Q.o) & (the Charact of G).:(Q.o) c= bool Den(o, A) by A15,FUNCT_1:def 12,MSUALG_1:def 11; then A16: dom Den(s2, G) c= dom Den(o, A) by RELAT_1:25; A17: Args(s2,G) = ((the Sorts of G)# * the Arity of S2).s2 by MSUALG_1:def 9 .= (the Sorts of G)# .((the Arity of S2).s2) by A15,FUNCT_1:23 .= (the Sorts of G)# .the_arity_of s2 by MSUALG_1:def 6 .= product(SG*the_arity_of s2) by MSUALG_1:def 3; then product p meets dom Den(o,A) by A12,A13,A14,A16,XBOOLE_0:3; hence s1 in the OperSymbols of S1 by A5; take p, s2; thus thesis by A12,A17; end; consider g being Function such that A18: dom g = the OperSymbols of S2 & rng g c= the OperSymbols of S1 & for s being set st s in the OperSymbols of S2 holds S[s,g.s] from NonUniqBoundFuncEx(A11); reconsider g as Function of the OperSymbols of S2, the OperSymbols of S1 by A18,FUNCT_2:4; take g; thus A19: dom f = the carrier of S2 & dom g = the OperSymbols of S2 & rng f c= the carrier of S1 & rng g c= the OperSymbols of S1 by FUNCT_2:def 1,RELSET_1:12; now let c be OperSymbol of S2; set s = (the ResultSort of S2).c; A20: R.s = ((the Sorts of G)*the ResultSort of S2).c & (f*the ResultSort of S2).c = f.s by FUNCT_2:21; R.s in rng R by A4,FUNCT_1:def 5; then R.s c= em.(R.s) by A10; then A21: R.s c= f.s by A4,FUNCT_1:23; consider p being FinSequence of P, o being OperSymbol of S2 such that A22: g.c = [Q-index_of c, p] & c = o & Args(o,G) c= product p by A18; reconsider p as Element of P* by FINSEQ_1:def 11; reconsider s2 = Q-index_of c as OperSymbol of A by A3,Def4; consider aa being Element of Args(o,G); (the Charact of G)|(Q.s2) is IndexedPartition of Den(s2, A) by A2,Def16 ; then rng ((the Charact of G)|(Q.s2)) is a_partition of Den(s2, A) by Def3; then o in Q.s2 & dom the Charact of G = the OperSymbols of S2 & (the Charact of G).:(Q.s2) is a_partition of Den(s2, A) by A22,Def4,PBOOLE:def 3,RELAT_1:148; then A23: Den(o, G) = (the Charact of G).o & (the Charact of G).o in (the Charact of G).:(Q.s2) & (the Charact of G).:(Q.s2) c= bool Den(s2, A) by FUNCT_1:def 12,MSUALG_1:def 11; then A24: dom Den(o,G) = Args(o,G) & dom Den(o,G) c= dom Den(s2,A) & aa in Args(o,G) by FUNCT_2:def 1,RELAT_1:25; then product p meets dom Den(s2,A) by A22,XBOOLE_0:3; then A25: Den(s2, A).:product p c= (the ResultSort of S1).(g.c) by A22,Def15; ((the Sorts of G)*the ResultSort of S2).c = Result(c,G) by MSUALG_1:def 10; then A26: rng Den(c,G) c= ((the Sorts of G)*the ResultSort of S2).c by RELSET_1:12 ; rng Den(c,G) = Den(c,G).:Args(c,G) by A22,A24,RELAT_1:146; then rng Den(c,G) c= Den(c,G).:product p & Den(c,G).:product p c= Den(s2,A).: product p by A22,A23,RELAT_1:156,157; then rng Den(c,G) c= Den(s2,A).:product p by XBOOLE_1:1; then rng Den(c,G) c= (the ResultSort of S1).(g.c) & Den(c,G).aa in rng Den(c,G) by A22,A24,A25,FUNCT_1:def 5,XBOOLE_1:1; then Den(c,G).aa in ((the Sorts of G)*the ResultSort of S2).c & Den(c,G).aa in (the ResultSort of S1).(g.c) by A26; then (f*the ResultSort of S2).c in P & ((the ResultSort of S1)*g).c in P & Den(c,G).aa in (f*the ResultSort of S2).c & Den(c,G).aa in ((the ResultSort of S1)*g).c by A6,A20,A21,FUNCT_2:21; hence (f*the ResultSort of S2).c = ((the ResultSort of S1)*g).c by Th3; end; hence f*the ResultSort of S2 = (the ResultSort of S1)*g by FUNCT_2:113; hereby let o be set, p be Function; assume o in the OperSymbols of S2; then reconsider s = o as OperSymbol of S2; assume A27: p = (the Arity of S2).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 p' being FinSequence of P, o' being OperSymbol of S2 such that A28: g.s = [Q-index_of s, p'] & s = o' & Args(o',G) c= product p' by A18; g.s in the OperSymbols of S1; then consider o1 being OperSymbol of A, p1 being Element of P* such that A29: g.s = [o1,p1] & product p1 meets dom Den(o1,A) by A5; p' = p1 & Q-index_of s = o1 by A28,A29,ZFMISC_1:33; then A30: (the Arity of S1).(g.o) = p' by A29,Def15; Args(o',G) = ((the Sorts of G)# * the Arity of S2).o' by MSUALG_1:def 9 .= (the Sorts of G)# .q by A28,FUNCT_2:21 .= product r by MSUALG_1:def 3; then em*r = p' by A10,A28,Th5; hence f*p = (the Arity of S1).(g.o) by A27,A30,RELAT_1:55; end; thus rng f c= the carrier of S1 by RELSET_1:12; thus the carrier of S1 c= rng f proof let s be set; assume s in the carrier of S1; then reconsider s as Element of P by Def15; consider a being Element of s; A31: R-index_of a in dom R & a in R.(R-index_of a) by Def4; then R.(R-index_of a) in rng R & em.(R.(R-index_of a)) = f.(R-index_of a) by FUNCT_1:23,def 5; then R.(R-index_of a) c= f.(R-index_of a) & f.(R-index_of a) in rng f & rng f c= P by A4,A10,A19,A31,Def15,FUNCT_1:def 5; hence thesis by A31,Th3; end; thus rng g c= the OperSymbols of S1 by A18; thus the OperSymbols of S1 c= rng g proof let s1 be set; assume s1 in the OperSymbols of S1; then consider o being OperSymbol of A, p being Element of P* such that A32: s1 = [o,p] & product p meets dom Den(o,A) by A5; consider a being set such that A33: a in product p & a in dom Den(o,A) by A32,XBOOLE_0:3; consider h being Function such that A34: a = h & dom h = dom p & for x being set st x in dom p holds h.x in p.x by A33,CARD_3:def 5; reconsider h as FinSequence by A34,Lm1; product p c= Funcs(dom p, Union p) by FUNCT_6:10; then rng p c= P & ex f being Function st h = f & dom f = dom p & rng f c= Union p by A33,A34,FINSEQ_1:def 4,FUNCT_2:def 2; then rng h c= Union p & Union p = union rng p & union rng p c= union P & union P = the carrier of A by EQREL_1:def 6,PROB_1:def 3,ZFMISC_1:95; then rng h c= the carrier of A by 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 A35: h in product r by Th7; A36: dom h = dom r & rng r c= rng R & rng p c= P by A35,CARD_3:18,FINSEQ_1:def 4; A37: Den(o,A) is_exactly_partitable_wrt P by Def11; now let x be set; assume x in dom r; then A38: h.x in p.x & h.x in r.x & r.x in rng r & p.x in rng p by A34,A35,A36,CARD_3:18,FUNCT_1:def 5; then consider c being set such that A39: c in P & r.x c= c by A7,A36,SETFAM_1:def 2; thus r.x c= p.x by A36,A38,A39,Th3; end; then A40: product r c= product p & product p c= dom Den(o,A) by A32,A34,A36,A37,Def10,CARD_3:38; then product r c= dom Den(o,A) by XBOOLE_1:1; then consider s2 being OperSymbol of S2 such that A41: (the Sorts of G)*the_arity_of s2 = r & s2 in Q.o by A2,Th33; consider p' being FinSequence of P, o' being OperSymbol of S2 such that A42: g.s2 = [Q-index_of s2, p'] & s2 = o' & Args(o',G) c= product p' by A18; A43: dom the Arity of S2 = the OperSymbols of S2 by FUNCT_2:def 1; Args(s2,G) = ((the Sorts of G)# * the Arity of S2).s2 by MSUALG_1:def 9 .= (the Sorts of G)# .((the Arity of S2).s2) by A43,FUNCT_1:23 .= (the Sorts of G)# .the_arity_of s2 by MSUALG_1:def 6 .= product r by A41,MSUALG_1:def 3; then p' = em*r & p = em*r & Q-index_of s2 = o by A3,A10,A40,A41,A42,Def4 ,Th5; hence thesis by A18,A32,A42,FUNCT_1:def 5; end; end;

Back to top