### The Mizar article:

### Order Sorted Quotient Algebra

**by****Josef Urban**

- Received September 19, 2002
Copyright (c) 2002 Association of Mizar Users

- MML identifier: OSALG_4
- [ MML identifier index ]

environ vocabulary AMI_1, MSUALG_1, FUNCT_1, RELAT_1, PBOOLE, BOOLE, EQREL_1, ZF_REFLE, QC_LANG1, PRALG_1, FINSEQ_1, TDGROUP, CARD_3, GROUP_6, ALG_1, FINSEQ_4, SEQM_3, PRALG_2, MSUALG_3, WELLORD1, MSUALG_4, OSALG_1, ORDERS_1, NATTRA_1, RELAT_2, FINSEQ_5, ARYTM_1, TARSKI, YELLOW18, YELLOW15, SETFAM_1, COH_SP, QUANTAL1, OSALG_4; notation ZFMISC_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, EQREL_1, SETFAM_1, STRUCT_0, XCMPLX_0, XREAL_0, ORDERS_1, ORDERS_3, NAT_1, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_4, FINSEQ_5, PBOOLE, WAYBEL_0, PRALG_1, MSUALG_1, MSUALG_3, PRALG_2, OSALG_1, OSALG_3, MSUALG_4, YELLOW18; constructors ORDERS_3, INT_1, NAT_1, FINSEQ_5, FINSEQ_4, MSUALG_3, WAYBEL_0, OSALG_3, MSUALG_4, EQREL_1, YELLOW18; clusters MSUALG_1, PRALG_1, MSUALG_3, PRALG_2, RELSET_1, SETFAM_1, STRUCT_0, FINSEQ_5, INT_1, RELAT_1, ORDERS_3, FILTER_1, SUBSET_1, OSALG_1, MSUALG_4, MSAFREE, PARTFUN1; requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM; definitions TARSKI, MSUALG_3, XBOOLE_0, OSALG_1, OSALG_3; theorems XBOOLE_0, XBOOLE_1, FUNCT_1, FUNCT_2, PBOOLE, CARD_3, MSUALG_1, PRALG_1, FINSEQ_4, MSUALG_5, SQUARE_1, OSALG_1, OSALG_3, RELAT_2, PRALG_2, ZFMISC_1, RELAT_1, RELSET_1, EQREL_1, MSUALG_3, MSUALG_6, MSAFREE, TARSKI, SYSREL, ORDERS_1, FINSEQ_1, AXIOMS, FINSEQ_3, ENUMSET1, FINSEQ_5, REAL_1, INT_1, ORDERS_3, PARTFUN1, WAYBEL_0, TOLER_1, GRFUNC_1, MSUALG_9, MSUALG_4, XCMPLX_1, FINSEQ_2; schemes FUNCT_1, ZFREFLE1, MSUALG_2, COMPTS_1, NAT_1, FUNCT_2; begin definition let R be non empty Poset; cluster Relation-yielding OrderSortedSet of R; existence proof set I = the carrier of R; consider R1 be Relation; deffunc F(set) = R1; consider f be Function such that A1: dom f = I & for x be set st x in I holds f.x = F(x) from Lambda; reconsider f as ManySortedSet of I by A1,PBOOLE:def 3; f is order-sorted proof let s1,s2 be Element of R such that s1 <= s2; f.s1 = R1 & f.s2 = R1 by A1; hence f.s1 c= f.s2; end; then reconsider f as OrderSortedSet of R; take f; for x be set st x in dom f holds f.x is Relation by A1; hence thesis by MSUALG_4:def 1; end; end; :: this is a stronger condition for relation than just being order-sorted definition let R be non empty Poset; let A,B be ManySortedSet of the carrier of R; let IT be ManySortedRelation of A,B; attr IT is os-compatible means :Def1: for s1,s2 being Element of R st s1 <= s2 for x,y being set st x in A.s1 & y in B.s1 holds [x,y] in IT.s1 iff [x,y] in IT.s2; end; definition let R be non empty Poset; let A,B be ManySortedSet of the carrier of R; cluster os-compatible ManySortedRelation of A,B; existence proof set I = the carrier of R; consider R1 be Relation such that A1: R1 = {}; deffunc F(set) = R1; consider f be Function such that A2: dom f = I & for x be set st x in I holds f.x = F(x) from Lambda; reconsider f as ManySortedSet of R by A2,PBOOLE:def 3; take f; set f1 = f; A3: for s1,s2 being Element of R st s1 <= s2 for x,y being set st x in A.s1 & y in B.s1 holds [x,y] in f1.s1 iff [x,y] in f1.s2 proof let s1,s2 be Element of R such that s1 <= s2; A4: f1.s1 = R1 by A2 .= f1.s2 by A2; let x,y be set such that x in A.s1 & y in B.s1; thus [x,y] in f1.s1 iff [x,y] in f1.s2 by A4; end; for i be set st i in I holds f.i is Relation of A.i,B.i proof let i be set; assume i in I; then f.i = {} by A1,A2; hence thesis by RELSET_1:25; end; then reconsider f2 = f1 as ManySortedRelation of A,B by MSUALG_4:def 2; f2 is os-compatible by A3,Def1; hence thesis; end; end; definition let R be non empty Poset; let A,B be ManySortedSet of the carrier of R; mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B; canceled; end; theorem Bze: for R being non empty Poset, A,B being ManySortedSet of the carrier of R, OR being ManySortedRelation of A,B holds OR is os-compatible implies OR is OrderSortedSet of R proof let R be non empty Poset, A,B be ManySortedSet of the carrier of R, OR be ManySortedRelation of A,B; assume A1: OR is os-compatible; set OR1 = OR; OR1 is order-sorted proof let s1,s2 be Element of R such that A2: s1 <= s2; for x,y being set holds [x,y] in OR.s1 implies [x,y] in OR.s2 proof let x,y be set such that A3: [x,y] in OR.s1; x in A.s1 & y in B.s1 by A3,ZFMISC_1:106; hence [x,y] in OR.s2 by A1,A2,A3,Def1; end; hence thesis by RELAT_1:def 3; end; hence thesis; end; definition let R be non empty Poset; let A,B be ManySortedSet of R; cluster os-compatible -> order-sorted ManySortedRelation of A,B; coherence by Bze; end; definition let R be non empty Poset; let A be ManySortedSet of the carrier of R; mode OrderSortedRelation of A is OrderSortedRelation of A,A; end; definition let S be OrderSortedSign, U1 be OSAlgebra of S; mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means :Def3: it is os-compatible; existence proof reconsider Y = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; consider X being OrderSortedRelation of Y; reconsider X1=X as ManySortedRelation of U1; take X1; thus thesis; end; end; :: REVISE: the definition of ManySorted diagonal from MSUALG_6 :: should be moved to MSUALG_4; the "compatible" attr from MSUALG_6 :: should replace the MSCongruence-like definition let S be OrderSortedSign, U1 be OSAlgebra of S; cluster MSEquivalence-like OrderSortedRelation of U1; existence proof deffunc F(Element of S) = id ((the Sorts of U1).$1); consider f be Function such that A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d) from LambdaB; reconsider f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3; for x be set st x in dom f holds f.x is Relation proof let x be set; assume x in dom f; then f.x = id ((the Sorts of U1).x) by A1; hence thesis; end; then reconsider f as ManySortedRelation of the carrier of S by MSUALG_4:def 1; for i be set st i in the carrier of S holds f.i is Relation of (the Sorts of U1).i,(the Sorts of U1).i proof let i be set; assume i in the carrier of S; then f.i = id ((the Sorts of U1).i) by A1; hence thesis; end; then reconsider f as ManySortedRelation of the Sorts of U1,the Sorts of U1 by MSUALG_4:def 2; reconsider f as ManySortedRelation of U1; for i be set, R be Relation of (the Sorts of U1).i st i in the carrier of S & f.i = R holds R is Equivalence_Relation of (the Sorts of U1).i proof let i be set, R be Relation of (the Sorts of U1).i; assume i in the carrier of S & f.i = R; then R = id ((the Sorts of U1).i) by A1; hence thesis; end; then A2: f is MSEquivalence_Relation-like by MSUALG_4:def 3; take f; set f1 = f; f1 is os-compatible proof let s1,s2 be Element of S such that A3: s1 <= s2; reconsider s3 = s1, s4 = s2 as Element of S; reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; X.s3 c= X.s4 by A3,OSALG_1:def 18; then A4: id(X.s1) c= id(X.s2) by SYSREL:33; A5: f1.s1 = id(X.s1) & f1.s2 = id(X.s2) by A1; let x,y be set such that A6: x in (the Sorts of U1).s1 & y in (the Sorts of U1).s1; thus [x,y] in f1.s1 implies [x,y] in f1.s2 by A4,A5; assume [x,y] in f1.s2; then x = y by A5,RELAT_1:def 10; hence [x,y] in f1.s1 by A5,A6,RELAT_1:def 10; end; hence thesis by A2,Def3,MSUALG_4:def 5; end; end; :: REVISE: we need the fact that id has the type, :: the original prf can be simplified definition let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster MSCongruence-like (MSEquivalence-like OrderSortedRelation of U1); existence proof deffunc F(Element of S) = id ((the Sorts of U1).$1); consider f be Function such that A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d) from LambdaB; reconsider f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3; for x be set st x in dom f holds f.x is Relation proof let x be set; assume x in dom f; then f.x = id ((the Sorts of U1).x) by A1; hence thesis; end; then reconsider f as ManySortedRelation of the carrier of S by MSUALG_4:def 1; for i be set st i in the carrier of S holds f.i is Relation of (the Sorts of U1).i,(the Sorts of U1).i proof let i be set; assume i in the carrier of S; then f.i = id ((the Sorts of U1).i) by A1; hence thesis; end; then reconsider f as ManySortedRelation of the Sorts of U1,the Sorts of U1 by MSUALG_4:def 2; reconsider f as ManySortedRelation of U1; for i be set, R be Relation of (the Sorts of U1).i st i in the carrier of S & f.i = R holds R is Equivalence_Relation of (the Sorts of U1).i proof let i be set, R be Relation of (the Sorts of U1).i; assume i in the carrier of S & f.i = R; then R = id ((the Sorts of U1).i) by A1; hence thesis; end; then f is MSEquivalence_Relation-like by MSUALG_4:def 3; then reconsider f as MSEquivalence-like ManySortedRelation of U1 by MSUALG_4:def 5; set f1 = f; f1 is os-compatible proof let s1,s2 be Element of S such that A2: s1 <= s2; reconsider s3 = s1, s4 = s2 as Element of S; reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; X.s3 c= X.s4 by A2,OSALG_1:def 18; then A3: id(X.s1) c= id(X.s2) by SYSREL:33; A4: f1.s1 = id(X.s1) & f1.s2 = id(X.s2) by A1; let x,y be set such that A5: x in (the Sorts of U1).s1 & y in (the Sorts of U1).s1; thus [x,y] in f1.s1 implies [x,y] in f1.s2 by A3,A4; assume [x,y] in f1.s2; then x = y by A4,RELAT_1:def 10; hence [x,y] in f1.s1 by A4,A5,RELAT_1:def 10; end; then reconsider f = f1 as MSEquivalence-like OrderSortedRelation of U1 by Def3; take f; for o be Element of the OperSymbols of S for x,y be Element of Args(o,U1) st (for n be Nat st n in dom x holds [x.n,y.n] in f.((the_arity_of o)/.n)) holds [Den(o,U1).x,Den(o,U1).y] in f.(the_result_sort_of o) proof let o be Element of the OperSymbols of S; let x,y be Element of Args(o,U1); assume A6: for n be Nat st n in dom x holds [x.n,y.n] in f.((the_arity_of o)/.n); A7: dom x = dom (the_arity_of o) & dom y = dom (the_arity_of o) by MSUALG_3:6; for a be set st a in dom (the_arity_of o) holds x.a = y.a proof let a be set; assume A8: a in dom (the_arity_of o); then reconsider n = a as Nat; A9: (the_arity_of o)/.n = (the_arity_of o).n by A8,FINSEQ_4:def 4; set ao = the_arity_of o; ao.n in rng ao by A8,FUNCT_1:def 5; then A10: f.(ao.n) = id ((the Sorts of U1).(ao.n)) by A1; [x.n,y.n] in f.(ao.n) by A6,A7,A8,A9; hence thesis by A10,RELAT_1:def 10; end; then A11: Den(o,U1).x = Den(o,U1).y by A7,FUNCT_1:9; set r = the_result_sort_of o; A12: f.r = id ((the Sorts of U1).r) by A1; A13: dom (the ResultSort of S) = the OperSymbols of S & rng (the ResultSort of S) c= the carrier of S by FUNCT_2:def 1; then A14: dom ((the Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort of S) by PBOOLE:def 3; Result(o,U1) = ((the Sorts of U1) * the ResultSort of S).o by MSUALG_1:def 10 .= (the Sorts of U1).((the ResultSort of S).o) by A13,A14,FUNCT_1:22 .= (the Sorts of U1).r by MSUALG_1:def 7; hence thesis by A11,A12,RELAT_1:def 10; end; hence thesis by MSUALG_4:def 6; end; end; definition let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; mode OSCongruence of U1 is MSCongruence-like (MSEquivalence-like OrderSortedRelation of U1); end; :: TODO: a smooth transition between Relations and Graphs would :: be useful here, the FinSequence approach seemed to me faster than :: transitive closure of R \/ R" .. maybe not, can be later a theorem :: all could be done generally for reflexive (or with small :: modification even non reflexive) Relations :: I found ex post that attributes disconnected and connected defined :: in ORDERS_3 have st. in common here, but the theory there is not developed :: suggested improvements: f connects x,y; x is_connected_with y; :: connected iff for x,y holds x is_connected_with y :: finally I found this is the EqCl from MSUALG_5 - should be merged definition let R be non empty Poset; func Path_Rel R -> Equivalence_Relation of the carrier of R means :Def4: for x,y being set holds [x,y] in it iff x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st 1 < len p & p.1 = x & p.(len p) = y & for n being Nat st 2 <= n & n <= len p holds [p.n,p.(n-1)] in the InternalRel of R or [p.(n-1),p.n] in the InternalRel of R; existence proof A1: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_1:def 4; defpred PC[set,set] means ex p being FinSequence of the carrier of R st 1 < len p & p.1 = $1 & p.(len p) = $2 & for n being Nat st 2 <= n & n <= len p holds [p.n,p.(n-1)] in the InternalRel of R or [p.(n-1),p.n] in the InternalRel of R; set P = { [x,y] where x,y is Element of R: x in the carrier of R & y in the carrier of R & PC[x,y]}; A2: for x,y being set holds [x,y] in P iff x in the carrier of R & y in the carrier of R & PC[x,y] proof let x,y be set; hereby assume [x,y] in P; then consider x1,y1 being Element of R such that A3: [x,y] = [x1,y1] and A4: x1 in the carrier of R & y1 in the carrier of R & PC[x1,y1]; x = x1 & y = y1 by A3,ZFMISC_1:33; hence x in the carrier of R & y in the carrier of R & PC[x,y] by A4; end; thus thesis; end; P c= [:the carrier of R, the carrier of R:] proof let z be set such that A6: z in P; consider x,y being Element of R such that A7: z = [x,y] & x in the carrier of R & y in the carrier of R & PC[x,y] by A6; thus thesis by A7,ZFMISC_1:106; end; then reconsider P1 = P as Relation of the carrier of R by RELSET_1:def 1; now let x be set; assume A8: x in the carrier of R; PC[x,x] proof set F = <*x,x*>; A9: F.1 = x & F.2 = x by FINSEQ_1:61; A10: len F = 2 by FINSEQ_1:61; rng F = {x,x} by FINSEQ_2:147 .= {x} by ENUMSET1:69; then rng F c= the carrier of R by A8,ZFMISC_1:37; then reconsider F1 = F as FinSequence of the carrier of R by FINSEQ_1:def 4; take F1; thus 1 < len F1 by A10; thus F1.1 = x & F1.(len F1) = x by A10,FINSEQ_1:61; let n1 be Nat such that A11: 2 <= n1 & n1 <= len F1; n1 = 2 by A10,A11,AXIOMS:21; hence thesis by A1,A8,A9,RELAT_2:def 1; end; hence [x,x] in P1 by A8; end; then P1 is_reflexive_in the carrier of R by RELAT_2:def 1; then A12: dom P1 = the carrier of R & field P1 = the carrier of R by ORDERS_1:98; now let x,y be set; assume A14: x in the carrier of R & y in the carrier of R & [x,y] in P1; then consider p being FinSequence of the carrier of R such that A15: 1 < len p & p.1 = x & p.(len p) = y & for n being Nat st 2 <= n & n <= len p holds [p.n,p.(n-1)] in the InternalRel of R or [p.(n-1),p.n] in the InternalRel of R by A2; PC[y,x] proof :: just counting, more builtin arithmetics would be nice take F = Rev p; A16: len F = len p by FINSEQ_5:def 3; thus 1 < len F by A15,FINSEQ_5:def 3; thus F.1 = y & F.(len F) = x by A15,A16,FINSEQ_5:65; let n1 be Nat such that A17: 2 <= n1 & n1 <= len F; A18: 1 <= n1 by A17,AXIOMS:22; A19: 2 - 1 <= n1 - 1 by A17,REAL_1:49; then 0 <= n1 - 1 by AXIOMS:22; then reconsider n1_1 = n1 - 1 as Nat by INT_1:16; n1 - 1 <= len F - 0 by A17,REAL_1:92; then A20: n1_1 in dom p by A16,A19,FINSEQ_3:27; then A21: n1 in dom p & (n1 - 1) in dom p by A16,A17,A18,FINSEQ_3:27; A22: F.(n1 - 1) = p.(len p - (n1 - 1) + 1) by A20,FINSEQ_5:61 .= p.((len p - n1) + 1 + 1) by XCMPLX_1:37 .= p.((len p - n1) + (1 + 1)) by XCMPLX_1:1 .= p.((len p - n1) + 2); set n2 = (len p - n1) + 2; 0 <= len p - n1 by A16,A17,SQUARE_1:12; then A23: 2 + 0 <= n2 by AXIOMS:24; len p - n1 <= len p - 2 by A17,REAL_1:92; then (len p - n1) + 2 <= len p - 2 + 2 by AXIOMS:24; then A24: (len p - n1) + 2 <= len p + ( 2 - 2) by XCMPLX_1:30; 0 <= n2 by A23,AXIOMS:22; then reconsider n2 = (len p - n1) + 2 as Nat by INT_1:16; p.(n2-1) = p.((len p - n1) + (2 - 1)) by XCMPLX_1:31 .= F.n1 by A21,FINSEQ_5:61; hence [F.n1,F.(n1-1)] in the InternalRel of R or [F.(n1-1),F.n1] in the InternalRel of R by A15,A22,A23,A24; end; hence [y,x] in P1 by A14; end; then A25: P1 is_symmetric_in the carrier of R by RELAT_2:def 3; now let x,y,z be set; assume A26: x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in P1 & [y,z] in P1; then PC[x,y] & PC[y,z] by A2; then consider p1,p2 being FinSequence of the carrier of R such that A27: 1 < len p1 & p1.1 = x & p1.(len p1) = y & for n being Nat st 2 <= n & n <= len p1 holds [p1.n,p1.(n-1)] in the InternalRel of R or [p1.(n-1),p1.n] in the InternalRel of R and A28: 1 < len p2 & p2.1 = y & p2.(len p2) = z & for n being Nat st 2 <= n & n <= len p2 holds [p2.n,p2.(n-1)] in the InternalRel of R or [p2.(n-1),p2.n] in the InternalRel of R; PC[x,z] proof take F = p1^p2; A29: len F = len p1 + len p2 by FINSEQ_1:35; 1 + 1 < len p1 + len p2 by A27,A28,REAL_1:67; hence 1 < len F by A29,AXIOMS:22; 1 in dom p1 by A27,FINSEQ_3:27; hence F.1 = x by A27,FINSEQ_1:def 7; len p2 in dom p2 by A28,FINSEQ_3:27; hence F.(len F) = z by A28,A29,FINSEQ_1:def 7; let n1 be Nat such that A30: 2 <= n1 & n1 <= len F; A31: 1 <= n1 by A30,AXIOMS:22; A32: 2 - 1 <= n1 - 1 by A30,REAL_1:49; then 0 <= n1 - 1 by AXIOMS:22; then reconsider n1_1 = n1 - 1 as Nat by INT_1:16; A33: n1 - 1 <= len F - 0 by A30,REAL_1:92; A34: len p1 + 1 <= n1 implies len p1 + 1 = n1 or len p1 + 1 < n1 by REAL_1:def 5; per cases by A34,INT_1:20; suppose A35: n1 <= len p1; then A36: n1 in dom p1 by A31,FINSEQ_3:27; n1 - 1 <= len p1 - 0 by A35,REAL_1:92; then n1_1 in dom p1 by A32,FINSEQ_3:27; then F.n1 = p1.n1 & F.(n1 -1) = p1.(n1 - 1) by A36,FINSEQ_1:def 7; hence [F.n1,F.(n1-1)] in the InternalRel of R or [F.(n1-1),F.n1] in the InternalRel of R by A27,A30,A35; suppose A37: len p1 + 1 < n1; len p1 < len p1 + 1 by REAL_1:69; then A38: len p1 < n1 by A37,AXIOMS:22; (len p1 + 1) - 1 < n1 - 1 by A37,REAL_1:54; then len p1 < n1 - 1 by XCMPLX_1:26; then A39: F.n1_1 = p2.(n1_1 - len p1) by A33,FINSEQ_1:37; 0 <= n1 - len p1 by A38,SQUARE_1:12; then reconsider k = n1 - len p1 as Nat by INT_1:16; A40: F.n1 = p2.k & F.(n1 - 1) = p2.(k - 1) by A30,A38,A39,FINSEQ_1:37, XCMPLX_1:21; 1 < n1 - len p1 by A37,REAL_1:86; then A41: 1 + 1 <= n1 - len p1 by INT_1:20; n1 <= len p1 + len p2 by A30,FINSEQ_1:35; then 2 <= k & k <= len p2 by A41,REAL_1:86; hence thesis by A28,A40; suppose A42: len p1 + 1 = n1; :: we misuse reflexivity here then A43: len p1 = n1 - 1 by XCMPLX_1:26; A44: len p1 in dom p1 by A27,FINSEQ_3:27; A45: len p1 + 1 <= len p1 + len p2 by A28,REAL_1:67; A46: F.(n1 - 1) = y by A27,A43,A44,FINSEQ_1:def 7; (len p1 + 1) - len p1 = 1 by XCMPLX_1:26; then F.n1 = y by A28,A42,A45,FINSEQ_1:36; hence thesis by A1,A26,A46,RELAT_2:def 1; end; hence [x,z] in P1 by A26; end; then P1 is_transitive_in the carrier of R by RELAT_2:def 8; then reconsider P1 = P as Equivalence_Relation of the carrier of R by A12,PARTFUN1:def 4,A25,RELAT_2:def 11,def 16; take P1; thus thesis by A2; end; uniqueness proof defpred PC1[set,set] means $1 in the carrier of R & $2 in the carrier of R & ex p being FinSequence of the carrier of R st 1 < len p & p.1 = $1 & p.(len p) = $2 & for n being Nat st 2 <= n & n <= len p holds [p.n,p.(n-1)] in the InternalRel of R or [p.(n-1),p.n] in the InternalRel of R; let X,Y be Equivalence_Relation of the carrier of R; assume A47: for x,y being set holds [x,y] in X iff PC1[x,y]; assume A48: for x,y being set holds [x,y] in Y iff PC1[x,y]; for x,y being set holds [x,y] in X iff [x,y] in Y proof let x,y be set; hereby assume [x,y] in X; then PC1[x,y] by A47; hence [x,y] in Y by A48; end; assume [x,y] in Y; then PC1[x,y] by A48; hence thesis by A47; end; hence thesis by RELAT_1:def 2; end; end; theorem Th2: for R being non empty Poset, s1,s2 being Element of R st s1 <= s2 holds [s1,s2] in Path_Rel R proof let R be non empty Poset, s1,s2 be Element of R such that A1: s1 <= s2; set p = <* s1, s2 *>; A2: len p = 2 by FINSEQ_1:61; then A3: 1 < len p & p.1 = s1 & p.(len p) = s2 by FINSEQ_1:61; for n being Nat st 2 <= n & n <= len p holds [p.n,p.(n-1)] in the InternalRel of R or [p.(n-1),p.n] in the InternalRel of R proof let n1 be Nat such that A4: 2 <= n1 & n1 <= len p; A5: n1 = 2 by A2,A4,AXIOMS:21; [s1,s2] in the InternalRel of R by A1,ORDERS_1:def 9; hence thesis by A3,A5,FINSEQ_1:61; end; hence [s1,s2] in Path_Rel R by A3,Def4; end; :: again, should be defined for Relations probably definition let R be non empty Poset; let s1,s2 be Element of R; pred s1 ~= s2 means :Def5: [s1,s2] in Path_Rel R; reflexivity proof set PR = Path_Rel R; field PR = the carrier of R by ORDERS_1:97; then PR is_reflexive_in the carrier of R by RELAT_2:def 9; hence thesis by RELAT_2:def 1; end; symmetry proof set PR = Path_Rel R; field PR = the carrier of R by ORDERS_1:97; then PR is_symmetric_in the carrier of R by RELAT_2:def 11; hence thesis by RELAT_2:def 3; end; end; theorem for R being non empty Poset, s1,s2,s3 being Element of R holds s1 ~= s2 & s2 ~= s3 implies s1 ~= s3 proof let R be non empty Poset; let s1,s2,s3 be Element of R; assume A1: s1 ~= s2 & s2 ~= s3; set PR = Path_Rel R; A2: [s1,s2] in PR & [s2,s3] in PR by A1,Def5; field PR = the carrier of R by ORDERS_1:97; then PR is_transitive_in the carrier of R by RELAT_2:def 16; then [s1,s3] in PR by A2,RELAT_2:def 8; hence thesis by Def5; end; :: do for Relations definition let R be non empty Poset; func Components R -> non empty (Subset-Family of R) equals :Def6: Class Path_Rel R; coherence; end; definition let R be non empty Poset; cluster -> non empty Element of Components R; coherence proof let X be Element of Components R; X in Components R; then X in Class Path_Rel R by Def6; then consider x being set such that A1: x in the carrier of R & X = Class(Path_Rel R,x) by EQREL_1:def 5; thus thesis by A1,EQREL_1:28; end; end; definition let R be non empty Poset; mode Component of R is Element of Components R; canceled; end; definition let R be non empty Poset; let s1 be Element of R; func CComp s1 -> Component of R equals :Def8: Class(Path_Rel R,s1); correctness proof set C = Class(Path_Rel R,s1); C in Class(Path_Rel R) by EQREL_1:def 5; hence thesis by Def6; end; end; theorem Th4: for R being non empty Poset, s1 be Element of R holds s1 in CComp(s1) proof let R be non empty Poset; let s1 be Element of R; s1 in Class(Path_Rel R,s1) by EQREL_1:28; hence thesis by Def8; end; theorem Th5: for R being non empty Poset, s1,s2 being Element of R st s1 <= s2 holds CComp(s1) = CComp(s2) proof let R be non empty Poset, s1,s2 be Element of R such that A1: s1 <= s2; [s1,s2] in Path_Rel R by A1,Th2; then Class(Path_Rel R,s1) = Class(Path_Rel R,s2) by EQREL_1:44; hence CComp(s1) = Class(Path_Rel R,s2) by Def8 .= CComp(s2) by Def8; end; definition let R be non empty Poset; let A be ManySortedSet of the carrier of R; let C be Component of R; func A-carrier_of C equals :Def9: union {A.s where s is Element of R: s in C}; correctness; end; theorem Th6: for R being non empty Poset, A being ManySortedSet of the carrier of R, s being (Element of R), x being set st x in A.s holds x in A-carrier_of CComp(s) proof let R be non empty Poset; let A be ManySortedSet of the carrier of R, s be (Element of R), x be set such that A1: x in A.s; s in CComp(s) by Th4; then A.s in {A.s1 where s1 is Element of R: s1 in CComp(s)}; then x in union {A.s1 where s1 is Element of R: s1 in CComp(s)} by A1,TARSKI:def 4; hence thesis by Def9; end; definition let R be non empty Poset; attr R is locally_directed means :Def10: for C being Component of R holds C is directed; end; theorem Th7: for R being discrete non empty Poset holds for x,y being Element of R st [x,y] in Path_Rel R holds x = y proof let R be discrete non empty Poset; let x,y be Element of R; assume [x,y] in Path_Rel R; then consider p being FinSequence of the carrier of R such that A1: 1 < len p & p.1 = x & p.(len p) = y & for n being Nat st 2 <= n & n <= len p holds [p.n,p.(n-1)] in the InternalRel of R or [p.(n-1),p.n] in the InternalRel of R by Def4; for n1 being Nat st 1 <= n1 & n1 <= len p holds p.n1 = x proof let n1 be Nat such that A2: 1 <= n1 & n1 <= len p; defpred P[Nat] means p.$1 <> x & 1 <= $1; assume A3: p.n1 <> x; then A4: ex k being Nat st P[k] by A2; consider k being Nat such that A5: P[k] & for n being Nat st P[n] holds k <= n from Min(A4); 1 < k by A1,A5,REAL_1:def 5; then A6: 1 + 1 <= k by INT_1:20; then A7: 1 + 1 - 1 <= k - 1 by REAL_1:49; then 0 <= k - 1 by AXIOMS:22; then reconsider k1 = k - 1 as Nat by INT_1:16; k <= n1 by A2,A3,A5; then A8: k <= len p by A2,AXIOMS:22; then k in dom p by A5,FINSEQ_3:27; then reconsider pk = p.k as Element of R by PARTFUN1:27; k1 < k by INT_1:26; then A9: p.k1 = x by A5,A7; per cases by A1,A6,A8,A9; suppose [pk,x] in the InternalRel of R; then pk <= x by ORDERS_1:def 9; hence contradiction by A5,ORDERS_3:1; suppose [x,pk] in the InternalRel of R; then x <= pk by ORDERS_1:def 9; hence contradiction by A5,ORDERS_3:1; end; hence thesis by A1; end; theorem Th8: for R being discrete non empty Poset, C being Component of R ex x being Element of R st C = {x} proof let R be discrete non empty Poset, C be Component of R; C in Components R; then C in Class Path_Rel R by Def6; then consider x being set such that A1: x in the carrier of R and A2: C = Class(Path_Rel R,x) by EQREL_1:def 5; reconsider x1 = x as Element of R by A1; take x1; for y being set holds y in C iff y = x1 proof let y be set; hereby assume A3: y in C; then A4: [y,x] in Path_Rel R by A2,EQREL_1:27; reconsider y1 = y as Element of R by A3; y1 = x1 by A4,Th7; hence y = x1; end; assume y = x1; hence y in C by A2,EQREL_1:28; end; hence thesis by TARSKI:def 1; end; theorem Th9: for R being discrete non empty Poset holds R is locally_directed proof let R be discrete non empty Poset; let C be Component of R; consider x being Element of R such that A1: C = {x} by Th8; for x,y being Element of R st x in C & y in C ex z being Element of R st z in C & x <= z & y <= z proof let x1,y1 be Element of R such that A2: x1 in C & y1 in C; A3: x1 = x & x = y1 by A1,A2,TARSKI:def 1; take x1; thus thesis by A2,A3; end; hence C is directed by WAYBEL_0:def 1; end; :: the system could generate this one from the following definition cluster locally_directed (non empty Poset); existence proof consider R being discrete non empty Poset; take R; thus thesis by Th9; end; end; definition cluster locally_directed OrderSortedSign; existence proof consider R being discrete OrderSortedSign; take R; thus thesis by Th9; end; end; definition cluster discrete -> locally_directed (non empty Poset); coherence by Th9; end; definition let S be locally_directed (non empty Poset); cluster -> directed Component of S; coherence by Def10; end; theorem Th10: {} is Equivalence_Relation of {} proof reconsider R = {} as Relation of {} by RELSET_1:25; R is_reflexive_in {} by RELAT_2:def 9,TOLER_1:1,2; then dom R = {} & field R = {} by ORDERS_1:98; hence thesis by TOLER_1:3,9,PARTFUN1:def 4; end; :: Much of what follows can be done generally for OrderSortedRelations :: of OrderSortedSets (and not just OrderSortedRelations of OSAlgebras), :: unfortunately, multiple inheritence would be needed to widen the :: latter to the former :: Classes on connected components definition let S be locally_directed OrderSortedSign; let A be OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of A; let C be Component of S; func CompClass(E,C) -> Equivalence_Relation of (the Sorts of A)-carrier_of C means :Def11: for x,y being set holds [x,y] in it iff ex s1 being Element of S st s1 in C & [x,y] in E.s1; existence proof defpred CC1[set,set] means ex s1 being Element of S st s1 in C & [$1,$2] in E.s1; A1: E is os-compatible by Def3; per cases; suppose A2: (the Sorts of A)-carrier_of C is empty; for x,y being set holds [x,y] in {} iff ex s1 being Element of S st s1 in C & [x,y] in E.s1 proof let x,y be set; thus [x,y] in {} implies ex s1 being Element of S st s1 in C & [x,y] in E.s1; assume ex s1 being Element of S st s1 in C & [x,y] in E.s1; then consider s1 being Element of S such that A3: s1 in C & [x,y] in E.s1; A4: x in (the Sorts of A).s1 by A3,ZFMISC_1:106; (the Sorts of A).s1 in {(the Sorts of A).s where s is Element of S: s in C} by A3; then x in union {(the Sorts of A).s where s is Element of S: s in C} by A4,TARSKI:def 4; hence thesis by A2,Def9; end; hence thesis by A2,Th10; suppose (the Sorts of A)-carrier_of C is non empty; then reconsider SAC = (the Sorts of A)-carrier_of C as non empty set; set CC = {[x,y] where x,y is Element of SAC: CC1[x,y]}; A5: for x,y being set holds [x,y] in CC iff CC1[x,y] proof let x,y be set; hereby assume [x,y] in CC; then consider x1,y1 being Element of SAC such that A6: [x,y] = [x1,y1] and A7: CC1[x1,y1]; thus CC1[x,y] by A6,A7; end; assume A8: CC1[x,y]; then consider s1 being Element of S such that A9: s1 in C & [x,y] in E.s1; A10: (the Sorts of A).s1 in {(the Sorts of A).s where s is Element of S: s in C} by A9; x in (the Sorts of A).s1 & y in (the Sorts of A).s1 by A9,ZFMISC_1:106; then x in union {(the Sorts of A).s where s is Element of S: s in C} & y in union {(the Sorts of A).s where s is Element of S: s in C} by A10,TARSKI:def 4; then reconsider x1 = x, y1 =y as Element of SAC by Def9; [x1,y1] in CC by A8; hence thesis; end; CC c= [:SAC, SAC:] proof let z be set such that A11: z in CC; consider x,y being Element of SAC such that A12: z = [x,y] & CC1[x,y] by A11; thus thesis by A12,ZFMISC_1:106; end; then reconsider P1 = CC as Relation of SAC by RELSET_1:def 1; now let x be set such that A13: x in SAC; reconsider x1 = x as Element of SAC by A13; x in union {(the Sorts of A).s where s is Element of S: s in C} by A13,Def9; then consider X being set such that A14: x in X and A15: X in {(the Sorts of A).s where s is Element of S: s in C} by TARSKI:def 4; consider s being Element of S such that A16: X = (the Sorts of A).s & s in C by A15; field(E.s) = (the Sorts of A).s by ORDERS_1:97; then E.s is_reflexive_in (the Sorts of A).s by RELAT_2:def 9; then [x,x] in E.s by A14,A16,RELAT_2:def 1; then [x1,x1] in CC by A16; hence [x,x] in P1; end; then P1 is_reflexive_in SAC by RELAT_2:def 1; then A17: dom P1 = SAC & field P1 = SAC by ORDERS_1:98; now let x,y be set such that A19: x in SAC & y in SAC & [x,y] in P1; reconsider x1 = x, y1 = y as Element of SAC by A19; consider x2,y2 being Element of SAC such that A20: [x,y] = [x2,y2] & CC1[x2,y2] by A19; A21: x = x2 & y = y2 by A20,ZFMISC_1:33; consider s5 being Element of S such that A22: s5 in C & [x2,y2] in E.s5 by A20; A23: x2 in (the Sorts of A).s5 & y2 in (the Sorts of A).s5 by A22,ZFMISC_1:106; field(E.s5) = (the Sorts of A).s5 by ORDERS_1:97; then E.s5 is_symmetric_in (the Sorts of A).s5 by RELAT_2:def 11; then [y,x] in E.s5 by A21,A22,A23,RELAT_2:def 3; then [y1,x1] in CC by A22; hence [y,x] in P1; end; then A24: P1 is_symmetric_in SAC by RELAT_2:def 3; now let x,y,z be set such that A25: x in SAC & y in SAC & z in SAC & [x,y] in P1 & [y,z] in P1; consider x2,y2 being Element of SAC such that A26: [x,y] = [x2,y2] & CC1[x2,y2] by A25; A27: x = x2 & y = y2 by A26,ZFMISC_1:33; consider y3,z3 being Element of SAC such that A28: [y,z] = [y3,z3] & CC1[y3,z3] by A25; A29: y = y3 & z = z3 by A28,ZFMISC_1:33; consider s5 being Element of S such that A30: s5 in C & [x2,y2] in E.s5 by A26; A31: x2 in (the Sorts of A).s5 & y2 in (the Sorts of A).s5 by A30,ZFMISC_1:106; consider s6 being Element of S such that A32: s6 in C & [y3,z3] in E.s6 by A28; A33: y3 in (the Sorts of A).s6 & z3 in (the Sorts of A).s6 by A32,ZFMISC_1:106; reconsider s5_1 = s5, s6_1 = s6 as Element of S; consider su being Element of S such that A34: su in C & s5_1 <= su & s6_1 <= su by A30,A32,WAYBEL_0:def 1; A35: [x2,y2] in E.su & [y3,z3] in E.su by A1,A30,A31,A32,A33,A34,Def1; then A36: x2 in (the Sorts of A).su & y2 in (the Sorts of A).su & z3 in (the Sorts of A).su by ZFMISC_1:106; field(E.su) = (the Sorts of A).su by ORDERS_1:97; then E.su is_transitive_in (the Sorts of A).su by RELAT_2:def 16; then [x2,z3] in E.su by A27,A29,A35,A36,RELAT_2:def 8; hence [x,z] in P1 by A27,A29,A34; end; then P1 is_transitive_in SAC by RELAT_2:def 8; then reconsider P1 as Equivalence_Relation of (the Sorts of A)-carrier_of C by A17,PARTFUN1:def 4,A24,RELAT_2:def 11,def 16; take P1; thus thesis by A5; end; uniqueness proof defpred CC1[set,set] means ex s1 being Element of S st s1 in C & [$1,$2] in E.s1; let X,Y be Equivalence_Relation of (the Sorts of A)-carrier_of C; assume A37: for x,y being set holds [x,y] in X iff CC1[x,y]; assume A38: for x,y being set holds [x,y] in Y iff CC1[x,y]; for x,y being set holds [x,y] in X iff [x,y] in Y proof let x,y be set; hereby assume [x,y] in X; then CC1[x,y] by A37; hence [x,y] in Y by A38; end; assume [x,y] in Y; then CC1[x,y] by A38; hence thesis by A37; end; hence thesis by RELAT_1:def 2; end; end; :: we could give a name to Class CompClass(E,C) :: restriction of Class CompClass(E,C) to A.s1 definition let S be locally_directed OrderSortedSign; let A be OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of A; let s1 be Element of S; func OSClass(E,s1) -> Subset of Class(CompClass(E,CComp(s1))) means :Def12: for z being set holds z in it iff ex x being set st x in (the Sorts of A).s1 & z = Class( CompClass(E,CComp(s1)), x); existence proof defpred CC1[set] means ex x being set st x in (the Sorts of A).s1 & $1 = Class( CompClass(E,CComp(s1)), x); set CS = Class(CompClass(E,CComp(s1))); set SAC = (the Sorts of A)-carrier_of CComp(s1); per cases; suppose A1: CS is empty; reconsider CS1 = {} as Subset of CS by XBOOLE_1:2; take CS1; let z be set; thus z in CS1 implies CC1[z]; assume CC1[z]; then consider x being set such that A2: x in (the Sorts of A).s1 & z = Class( CompClass(E,CComp(s1)), x); x in SAC by A2,Th6; hence thesis by A1,A2,EQREL_1:def 5; suppose CS is non empty; then reconsider CS1 = CS as non empty Subset-Family of SAC; set CC = {x where x is Element of CS1: CC1[x]}; now let x be set; assume x in CC; then consider y being Element of CS1 such that A3: x = y & CC1[y]; thus x in CS1 by A3; end; then reconsider CC2 = CC as Subset of CS by TARSKI:def 3; take CC2; for x being set holds x in CC iff CC1[x] proof let x be set; hereby assume x in CC; then consider x1 being Element of CS1 such that A4: x = x1 & CC1[x1]; thus CC1[x] by A4; end; assume A5: CC1[x]; then consider y being set such that A6: y in (the Sorts of A).s1 and A7: x = Class( CompClass(E,CComp(s1)), y); s1 in CComp(s1) by Th4; then (the Sorts of A).s1 in {(the Sorts of A).s where s is Element of the carrier of S: s in CComp(s1)}; then y in union {(the Sorts of A).s where s is Element of the carrier of S: s in CComp(s1)} by A6,TARSKI:def 4; then y in SAC by Def9; then x in Class( CompClass(E,CComp(s1))) by A7,EQREL_1:def 5; hence x in CC by A5; end; hence thesis; end; uniqueness proof defpred CC1[set] means ex x being set st x in (the Sorts of A).s1 & $1 = Class( CompClass(E,CComp(s1)), x); let X,Y be Subset of Class(CompClass(E,CComp(s1))); assume A8: for x being set holds x in X iff CC1[x]; assume A9: for x being set holds x in Y iff CC1[x]; for x being set holds x in X iff x in Y proof let x be set; hereby assume x in X; then CC1[x] by A8; hence x in Y by A9; end; assume x in Y; then CC1[x] by A9; hence thesis by A8; end; hence thesis by TARSKI:2; end; end; definition let S be locally_directed OrderSortedSign; let A be non-empty OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of A; let s1 be Element of S; cluster OSClass(E,s1) -> non empty; coherence proof consider x being set such that A1: x in (the Sorts of A).s1 by XBOOLE_0:def 1; Class( CompClass(E,CComp(s1)), x) in OSClass(E,s1) by A1,Def12; hence thesis; end; end; theorem Th11: for S being locally_directed OrderSortedSign, A being OSAlgebra of S, E being (MSEquivalence-like OrderSortedRelation of A), s1,s2 being Element of S st s1 <= s2 holds OSClass(E,s1) c= OSClass(E,s2) proof let S be locally_directed OrderSortedSign; let A be OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of A; let s1,s2 be Element of S; reconsider s3 = s1, s4 = s2 as Element of S; assume A1: s1 <= s2; then A2: CComp(s1) = CComp(s2) by Th5; thus OSClass(E,s1) c= OSClass(E,s2) proof let z be set such that A3: z in OSClass(E,s1); consider x being set such that A4: x in (the Sorts of A).s1 & z = Class( CompClass(E,CComp(s1)), x) by A3,Def12; reconsider SO = the Sorts of A as OrderSortedSet of S by OSALG_1:17; SO.s3 c= SO.s4 by A1,OSALG_1:def 18; hence thesis by A2,A4,Def12; end; end; :: finally, this is analogy of the Many-Sorted Class E for order-sorted E :: this definition should work for order-sorted MSCongruence too :: if non-empty not needed, prove the following cluster definition let S be locally_directed OrderSortedSign; let A be OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of A; func OSClass E -> OrderSortedSet of S means :Def13: for s1 being Element of S holds it.s1 = OSClass(E,s1); existence proof deffunc F(Element of S) = OSClass(E,$1); consider f being Function such that A1: dom f = the carrier of S and A2: for i being Element of S holds f.i = F(i) from LambdaB; reconsider f1 = f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3; set f2 = f1; f2 is order-sorted proof let s1,s2 be Element of S such that A3: s1 <= s2; f2.s1 = OSClass(E,s1) & f2.s2 = OSClass(E,s2) by A2; hence f2.s1 c= f2.s2 by A3,Th11; end; hence thesis by A2; end; uniqueness proof let X,Y be OrderSortedSet of S; assume A4: for s1 being Element of S holds X.s1 = OSClass(E,s1); assume A5: for s1 being Element of S holds Y.s1 = OSClass(E,s1); now let s1 be set; assume s1 in the carrier of S; then reconsider s2 = s1 as Element of S; thus X.s1 = OSClass(E,s2) by A4 .= Y.s1 by A5; end; hence X = Y by PBOOLE:3; end; end; definition let S be locally_directed OrderSortedSign; let A be non-empty OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of A; cluster OSClass E -> non-empty; coherence proof for i being set st i in the carrier of S holds (OSClass E).i is non empty proof let i be set such that A1: i in the carrier of S; reconsider s = i as Element of S by A1; (OSClass E).s = OSClass( E,s) by Def13; hence (OSClass E).i is non empty; end; hence thesis by PBOOLE:def 16; end; end; :: order-sorted equiv of Class(R,x) definition let S be locally_directed OrderSortedSign; let U1 be non-empty OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of U1; let s be Element of S; let x be Element of (the Sorts of U1).s; func OSClass(E,x) -> Element of OSClass(E,s) equals :Def14: Class( CompClass(E, CComp(s)), x); correctness by Def12; end; theorem for R being locally_directed (non empty Poset), x,y being Element of R st (ex z being Element of R st z <= x & z <= y) holds ex u being Element of R st x <= u & y <= u proof let R be locally_directed (non empty Poset), x,y be Element of R such that A1: (ex z being Element of R st z <= x & z <= y); reconsider x1 = x,y1 = y as Element of R; consider z being Element of R such that A2: z <= x & z <= y by A1; CComp z = CComp(x) & CComp(z) = CComp(y) by A2,Th5; then x in CComp(z) & y in CComp(z) by Th4; then ex u being Element of R st u in CComp(z) & x1 <= u & y1 <= u by WAYBEL_0:def 1; hence thesis; end; theorem Th13: for S be locally_directed OrderSortedSign, U1 be non-empty OSAlgebra of S, E be (MSEquivalence-like OrderSortedRelation of U1), s be (Element of S), x,y be Element of (the Sorts of U1).s holds OSClass(E,x) = OSClass(E,y) iff [x,y] in E.s proof let S be locally_directed OrderSortedSign; let U1 be non-empty OSAlgebra of S; let E be MSEquivalence-like OrderSortedRelation of U1; let s be Element of S; let x,y be Element of (the Sorts of U1).s; reconsider SU = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; A1: x in (the Sorts of U1)-carrier_of CComp(s) by Th6; A2: s in CComp(s) by Th4; A3: E is os-compatible by Def3; hereby assume OSClass(E,x) = OSClass(E,y); then Class( CompClass(E, CComp(s)), x) = OSClass(E,y) by Def14 .= Class( CompClass(E, CComp(s)), y) by Def14; then [x,y] in CompClass(E, CComp(s)) by A1,EQREL_1:44; then consider s1 being Element of S such that A4: s1 in CComp(s) & [x,y] in E.s1 by Def11; reconsider sn1 = s, s1_1 = s1 as Element of S; A5: x in SU.s1_1 & y in SU.s1_1 by A4,ZFMISC_1:106; consider s2 being Element of S such that A6: s2 in CComp(s) & s1_1 <= s2 & sn1 <= s2 by A2,A4,WAYBEL_0:def 1; [x,y] in E.s2 by A3,A4,A5,A6,Def1; hence [x,y] in E.s by A3,A6,Def1; end; assume A7: [x,y] in E.s; A8: x in (the Sorts of U1)-carrier_of CComp(s) by Th6; s in CComp(s) by Th4; then [x,y] in CompClass(E, CComp(s)) by A7,Def11; then Class( CompClass(E, CComp(s)), x) = Class( CompClass(E, CComp(s)), y) by A8,EQREL_1:44; hence OSClass(E,x) = Class( CompClass(E, CComp(s)), y) by Def14 .= OSClass(E ,y) by Def14; end; theorem Th14: for S be locally_directed OrderSortedSign, U1 be non-empty OSAlgebra of S, E be (MSEquivalence-like OrderSortedRelation of U1), s1,s2 be (Element of S), x be Element of (the Sorts of U1).s1 st s1 <= s2 holds for y being Element of (the Sorts of U1).s2 st y = x holds OSClass(E,x) = OSClass(E,y) proof let S be locally_directed OrderSortedSign, U1 be non-empty OSAlgebra of S, E be (MSEquivalence-like OrderSortedRelation of U1), s1,s2 be (Element of S), x be Element of (the Sorts of U1).s1; assume s1 <= s2; then A1: CComp(s1) = CComp(s2) by Th5; let y be Element of (the Sorts of U1).s2 such that A2: y = x; thus OSClass(E,x) = Class( CompClass(E, CComp(s2)), y) by A1,A2,Def14 .= OSClass(E,y) by Def14; end; begin :::::::::::::::::::::::::::::::::::::: :: Order Sorted Quotient Algebra :: :::::::::::::::::::::::::::::::::::::: :: take care (or even prove counterexample) - order-sorted :: ManySortedFunction generaly doesnot exist reserve S for locally_directed OrderSortedSign; reserve o for Element of the OperSymbols of S; :: multiclasses definition let S,o; let A be non-empty OSAlgebra of S; let R be OSCongruence of A; let x be Element of Args(o,A); func R #_os x -> Element of product ((OSClass R) * (the_arity_of o)) means :Def15: for n be Nat st n in dom (the_arity_of o) ex y being Element of (the Sorts of A).((the_arity_of o)/.n) st y = x.n & it.n = OSClass(R, y); existence proof set ar = the_arity_of o, da = dom ar; defpred P[set,set] means for n be Nat st n = $1 holds ex y being Element of (the Sorts of A).((the_arity_of o)/.n) st y = x.n & $2 = OSClass(R, y); A1: for k be set st k in da ex u be set st P[k,u] proof let k be set; assume A2: k in da; then reconsider n = k as Nat; reconsider y = x.n as Element of (the Sorts of A).((the_arity_of o)/.n) by A2,MSUALG_6:2; take OSClass(R,y); thus thesis; end; consider f be Function such that A3: dom f = da & for x be set st x in da holds P[x,f.x] from NonUniqFuncEx(A1); A4: dom ((OSClass R) * ar) = da by PBOOLE:def 3; for y be set st y in dom ((OSClass R) * ar) holds f.y in ((OSClass R) * ar).y proof let y be set; assume A5: y in dom ((OSClass R) * ar); then A6: ((OSClass R) * ar).y = (OSClass R).(ar.y) by FUNCT_1:22; ar.y in rng ar by A4,A5,FUNCT_1:def 5; then reconsider s = ar.y as Element of S; reconsider n = y as Nat by A5; consider z being Element of (the Sorts of A).((the_arity_of o)/.n) such that A7: z = x.n & f.n = OSClass(R, z) by A3,A4,A5; ((ar)/.n) = ar.n by A4,A5,FINSEQ_4:def 4; then f.y in OSClass (R,s) by A7; hence thesis by A6,Def13; end; then reconsider f as Element of product ((OSClass R) * ar) by A3,A4,CARD_3:18; take f; let n be Nat; assume n in da; hence thesis by A3; end; uniqueness proof let F,G be Element of product ((OSClass R) * (the_arity_of o)); assume that A8: for n be Nat st n in dom (the_arity_of o) holds ex y being Element of (the Sorts of A).((the_arity_of o)/.n) st y = x.n & F.n = OSClass(R, y) and A9: for n be Nat st n in dom (the_arity_of o) holds ex y being Element of (the Sorts of A).((the_arity_of o)/.n) st y = x.n & G.n = OSClass(R, y); dom F = dom ((OSClass R) * (the_arity_of o)) & dom G = dom ((OSClass R) * (the_arity_of o)) by CARD_3:18; then A10: dom F = dom (the_arity_of o) & dom G = dom (the_arity_of o) by PBOOLE:def 3; for y be set st y in dom (the_arity_of o) holds F.y = G.y proof let y be set; assume A11: y in dom (the_arity_of o); then reconsider n = y as Nat; consider z being Element of (the Sorts of A).((the_arity_of o)/.n) such that A12: z = x.n & F.n = OSClass(R, z) by A8,A11; consider z1 being Element of (the Sorts of A).((the_arity_of o)/.n) such that A13: z1 = x.n & G.n = OSClass(R, z1) by A9,A11; thus thesis by A12,A13; end; hence thesis by A10,FUNCT_1:9; end; end; :: the quotient will be different for order-sorted; :: this def seems ok for order-sorted definition let S,o; let A be non-empty OSAlgebra of S; let R be OSCongruence of A; func OSQuotRes(R,o) -> Function of ((the Sorts of A) * the ResultSort of S).o, ((OSClass R) * the ResultSort of S).o means :Def16: for x being Element of (the Sorts of A).(the_result_sort_of o) holds it.x = OSClass(R,x); existence proof set rs = (the_result_sort_of o), D = (the Sorts of A).rs; deffunc F(Element of D) = OSClass(R,$1); consider f be Function such that A1: dom f = D & for d be Element of D holds f.d = F(d) from LambdaB; A2: o in the OperSymbols of S; A3: dom (the ResultSort of S) = the OperSymbols of S & rng (the ResultSort of S) c= the carrier of S by FUNCT_2:def 1; o in dom ((the Sorts of A)*(the ResultSort of S)) by A2,PBOOLE:def 3; then A4: ((the Sorts of A) * the ResultSort of S).o = (the Sorts of A).((the ResultSort of S).o) by FUNCT_1:22 .= D by MSUALG_1:def 7; dom ((OSClass R) * the ResultSort of S) = dom (the ResultSort of S) by A3,PBOOLE:def 3; then A5: ((OSClass R) * the ResultSort of S).o = (OSClass R).((the ResultSort of S).o) by A3,FUNCT_1:22 .= (OSClass R).rs by MSUALG_1:def 7; for x be set st x in D holds f.x in (OSClass R).rs proof let x be set; assume x in D; then reconsider x1 = x as Element of D; f.x1 = OSClass(R,x1) by A1; then f.x1 in OSClass (R,rs); hence thesis by Def13; end; then reconsider f as Function of ((the Sorts of A) * the ResultSort of S).o, ((OSClass R) * the ResultSort of S).o by A1,A4,A5,FUNCT_2:5; take f; thus thesis by A1; end; uniqueness proof let f,g be Function of ((the Sorts of A) * the ResultSort of S).o, ((OSClass R) * the ResultSort of S).o; set SA = the Sorts of A, RS = the ResultSort of S, rs = the_result_sort_of o; assume that A6: for x being Element of SA.rs holds f.x = OSClass(R,x) and A7: for x being Element of SA.rs holds g.x = OSClass(R,x); A8: o in the OperSymbols of S; A9: dom RS = the OperSymbols of S & rng RS c= the carrier of S by FUNCT_2:def 1; o in dom (SA*RS) by A8,PBOOLE:def 3; then A10: (SA * RS).o = SA.(RS.o) by FUNCT_1:22 .= SA.rs by MSUALG_1:def 7; dom ((OSClass R) * RS) = dom RS by A9,PBOOLE:def 3; then ((OSClass R) * RS).o = (OSClass R).(RS.o) by A9,FUNCT_1:22 .= (OSClass R).rs by MSUALG_1:def 7; then A11: dom f = SA.rs & rng f c= (OSClass R).rs & dom g = SA.rs & rng g c= (OSClass R).rs by A10,FUNCT_2:def 1; now let x be set; assume x in SA.rs; then reconsider x1 = x as Element of SA.rs; f.x1 = OSClass(R,x1) & g.x1 = OSClass(R,x1) by A6,A7; hence f.x = g.x; end; hence thesis by A11,FUNCT_1:9; end; func OSQuotArgs(R,o) -> Function of ((the Sorts of A)# * the Arity of S).o, ((OSClass R)# * the Arity of S).o means for x be Element of Args(o,A) holds it.x = R #_os x; existence proof set D = Args(o,A); deffunc F(Element of D) = R #_os $1; consider f be Function such that A12: dom f = D & for d be Element of D holds f.d = F(d) from LambdaB; A13: D = ((the Sorts of A)# * the Arity of S).o by MSUALG_1:def 9; A14: o in the OperSymbols of S; then o in dom ((the Sorts of A)# * the Arity of S) by PBOOLE:def 3; then A15: ((the Sorts of A)# * the Arity of S).o = (the Sorts of A)#.((the Arity of S).o) by FUNCT_1:22 .= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 6; set ao = the_arity_of o; o in dom ((OSClass R)# * the Arity of S) by A14,PBOOLE:def 3; then A16: ((OSClass R)# * the Arity of S).o = (OSClass R)#.((the Arity of S).o) by FUNCT_1:22 .= (OSClass R)#.ao by MSUALG_1:def 6; for x be set st x in (the Sorts of A)#.ao holds f.x in (OSClass R)#.ao proof let x be set; assume x in (the Sorts of A)#.ao; then reconsider x1 = x as Element of D by A15,MSUALG_1:def 9; A17: f.x1 = R #_os x1 by A12; (OSClass R)#.ao = product((OSClass R)*ao) by MSUALG_1:def 3; hence thesis by A17; end; then reconsider f as Function of ((the Sorts of A)# * the Arity of S).o, ((OSClass R)# * the Arity of S).o by A12,A13,A15,A16,FUNCT_2:5; take f; thus thesis by A12; end; uniqueness proof let f,g be Function of ((the Sorts of A)# * the Arity of S).o, ((OSClass R)# * the Arity of S).o; assume that A18: for x be Element of Args(o,A) holds f.x = R #_os x and A19: for x be Element of Args(o,A) holds g.x = R #_os x; o in the OperSymbols of S; then o in dom ((the Sorts of A)# * the Arity of S) by PBOOLE:def 3; then A20: ((the Sorts of A)# * the Arity of S).o = (the Sorts of A)#.((the Arity of S).o) by FUNCT_1:22 .= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 6; set ao = the_arity_of o; A21: dom f = (the Sorts of A)#.ao & dom g = (the Sorts of A)#.ao by A20,FUNCT_2:def 1; now let x be set; assume x in (the Sorts of A)#.ao; then reconsider x1 = x as Element of Args(o,A) by A20,MSUALG_1:def 9; f.x1 = R #_os x1 & g.x1 = R #_os x1 by A18,A19; hence f.x = g.x; end; hence thesis by A21,FUNCT_1:9; end; end; definition let S; let A be non-empty OSAlgebra of S; let R be OSCongruence of A; func OSQuotRes R -> ManySortedFunction of ((the Sorts of A) * the ResultSort of S), ((OSClass R) * the ResultSort of S) means for o being OperSymbol of S holds it.o = OSQuotRes(R,o); existence proof set O = the OperSymbols of S; defpred P[set,set] means for o be OperSymbol of S st o = $1 holds $2 = OSQuotRes(R,o); A1: for x be set st x in O ex y be set st P[x,y] proof let x be set; assume x in O; then reconsider x1 = x as OperSymbol of S; take OSQuotRes(R,x1); thus thesis; end; consider f be Function such that A2: dom f = O & for x be set st x in O holds P[x,f.x] from NonUniqFuncEx(A1); reconsider f as ManySortedSet of O by A2,PBOOLE:def 3; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider x1 = x as OperSymbol of S by A2; f.x1 = OSQuotRes(R,x1) by A2; hence thesis; end; then reconsider f as ManySortedFunction of O by PRALG_1:def 15; for i be set st i in O holds f.i is Function of ((the Sorts of A) * the ResultSort of S).i, ((OSClass R) * the ResultSort of S).i proof let i be set; assume i in O; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotRes(R,i1) by A2; hence thesis; end; then reconsider f as ManySortedFunction of ((the Sorts of A) * the ResultSort of S), ((OSClass R) * the ResultSort of S) by MSUALG_1:def 2; take f; thus thesis by A2; end; uniqueness proof let f,g be ManySortedFunction of ((the Sorts of A) * the ResultSort of S), ((OSClass R) * the ResultSort of S); assume that A3: for o being OperSymbol of S holds f.o = OSQuotRes(R,o) and A4: for o being OperSymbol of S holds g.o = OSQuotRes(R,o); now let i be set; assume i in the OperSymbols of S; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotRes(R,i1) & g.i1 = OSQuotRes(R,i1) by A3,A4; hence f.i = g.i; end; hence thesis by PBOOLE:3; end; func OSQuotArgs R -> ManySortedFunction of (the Sorts of A)# * the Arity of S, (OSClass R)# * the Arity of S means for o be OperSymbol of S holds it.o = OSQuotArgs(R,o); existence proof set O = the OperSymbols of S; defpred P[set,set] means for o be OperSymbol of S st o = $1 holds $2 = OSQuotArgs(R,o); A5: for x be set st x in O ex y be set st P[x,y] proof let x be set; assume x in O; then reconsider x1 = x as OperSymbol of S; take OSQuotArgs(R,x1); thus thesis; end; consider f be Function such that A6: dom f = O & for x be set st x in O holds P[x,f.x] from NonUniqFuncEx(A5); reconsider f as ManySortedSet of O by A6,PBOOLE:def 3; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider x1 = x as OperSymbol of S by A6; f.x1 = OSQuotArgs(R,x1) by A6; hence thesis; end; then reconsider f as ManySortedFunction of O by PRALG_1:def 15; for i be set st i in O holds f.i is Function of ((the Sorts of A)# * the Arity of S).i, ((OSClass R)# * the Arity of S).i proof let i be set; assume i in O; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotArgs(R,i1) by A6; hence thesis; end; then reconsider f as ManySortedFunction of ((the Sorts of A)# * the Arity of S), ((OSClass R)# * the Arity of S) by MSUALG_1:def 2; take f; thus thesis by A6; end; uniqueness proof let f,g be ManySortedFunction of ((the Sorts of A)# * the Arity of S), ((OSClass R)# * the Arity of S); assume that A7: for o being OperSymbol of S holds f.o = OSQuotArgs(R,o) and A8: for o being OperSymbol of S holds g.o = OSQuotArgs(R,o); now let i be set; assume i in the OperSymbols of S; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotArgs(R,i1) & g.i1 = OSQuotArgs(R,i1) by A7,A8; hence f.i = g.i; end; hence thesis by PBOOLE:3; end; end; theorem Th15: for A be non-empty OSAlgebra of S, R be OSCongruence of A, x be set st x in ((OSClass R)# * the Arity of S).o ex a be Element of Args(o,A) st x = R #_os a proof let A be non-empty OSAlgebra of S, R be OSCongruence of A, x be set; assume A1: x in ((OSClass R)# * the Arity of S).o; set ar = the_arity_of o; A2: ar = (the Arity of S).o by MSUALG_1:def 6; then ((OSClass R)# * the Arity of S).o = product ((OSClass R) * ar) by MSAFREE:1; then consider f be Function such that A3: f = x & dom f = dom ((OSClass R) * ar) & for y be set st y in dom ((OSClass R) * ar) holds f.y in ((OSClass R) * ar).y by A1,CARD_3:def 5; A4: dom ((OSClass R) * ar) = dom ar by PBOOLE:def 3; A5: for n be Nat st n in dom f holds f.n in OSClass (R,((ar)/.n)) proof let n be Nat; assume A6: n in dom f; then A7: ar.n = ((ar)/.n) by A3,A4,FINSEQ_4:def 4; reconsider s = ((ar)/.n) as Element of S; ((OSClass R) * ar).n = (OSClass R).s by A3,A6,A7,FUNCT_1:22 .= OSClass (R,s) by Def13; hence thesis by A3,A6; end; defpred P[set,set] means $2 in (the Sorts of A).((ar)/.$1) & $2 in f.$1; A8: for a be set st a in dom f ex b be set st P[a,b] proof let a be set; assume A9: a in dom f; then reconsider n = a as Nat by A3; reconsider s = ((ar)/.a) as Element of S; f.n in OSClass (R,s) by A5,A9; then consider x being set such that A10: x in (the Sorts of A).s & f.n = Class( CompClass(R,CComp(s)), x) by Def12; take x; x in (the Sorts of A)-carrier_of CComp(s) by A10,Th6; hence thesis by A10,EQREL_1:28; end; consider g be Function such that A11: dom g = dom f & for a be set st a in dom f holds P[a,g.a] from NonUniqFuncEx(A8); A12: Args(o,A) = ((the Sorts of A)# * (the Arity of S)).o by MSUALG_1:def 9 .= product ((the Sorts of A) * ar) by A2,MSAFREE:1; dom (the Sorts of A) = the carrier of S by PBOOLE:def 3; then rng ar c= dom (the Sorts of A); then A13: dom g = dom ((the Sorts of A) * ar) by A3,A4,A11,RELAT_1:46; for y be set st y in dom ((the Sorts of A) * ar) holds g.y in ((the Sorts of A) * ar).y proof let y be set; assume A14: y in dom ((the Sorts of A) * ar); then reconsider n = y as Nat; A15: ar.n = ((ar)/.n) by A3,A4,A11,A13,A14,FINSEQ_4:def 4; reconsider s = ((ar)/.n) as Element of S; g.n in (the Sorts of A).s by A11,A13,A14; hence thesis by A14,A15,FUNCT_1:22; end; then reconsider g as Element of Args(o,A) by A12,A13,CARD_3:18; take g; A16: dom (R #_os g) = dom ((OSClass R) * ar) by CARD_3:18; for x being set st x in dom ar holds f.x = (R #_os g).x proof let x be set; assume A17: x in dom ar; then reconsider n = x as Nat; reconsider s = ((ar)/.n) as Element of S; consider z being Element of (the Sorts of A).((the_arity_of o)/.n) such that A18: z = g.n & (R #_os g).n = OSClass(R, z) by A17,Def15; A19: g.n in (the Sorts of A).((ar)/.n) & g.n in f.n by A3,A4,A11,A17; f.n in OSClass (R,s) by A3,A4,A5,A17; then consider u being set such that A20: u in (the Sorts of A).s & f.n = Class( CompClass(R,CComp(s)), u) by Def12; u in (the Sorts of A)-carrier_of CComp(s) by A20,Th6; then f.n = Class( CompClass(R,CComp(s)), g.n) by A19,A20,EQREL_1:31; hence thesis by A18,Def14; end; hence thesis by A3,A4,A16,FUNCT_1:9; end; definition let S,o; let A be non-empty OSAlgebra of S; let R be OSCongruence of A; func OSQuotCharact(R,o) -> Function of ((OSClass R)# * the Arity of S).o, ((OSClass R) * the ResultSort of S).o means :Def20: for a be Element of Args(o,A) st R #_os a in ((OSClass R)# * the Arity of S).o holds it.(R #_os a) = ((OSQuotRes(R,o)) * (Den(o,A))).a; existence proof set Ca = ((OSClass R)# * the Arity of S).o, Cr = ((OSClass R) * the ResultSort of S).o; defpred P[set,set] means for a be Element of Args(o,A) st $1 = R #_os a holds $2 = ((OSQuotRes(R,o)) * (Den(o,A))).a; A1: for x be set st x in Ca ex y be set st y in Cr & P[x,y] proof let x be set; assume x in Ca; then consider a be Element of Args(o,A) such that A2: x = R #_os a by Th15 ; take y = ((OSQuotRes(R,o)) * (Den(o,A))).a; A3: dom Den(o,A) = Args(o,A) & rng Den(o,A) c= Result(o,A) by FUNCT_2:def 1; A4: o in the OperSymbols of S; set ro = the_result_sort_of o, ar = the_arity_of o; A5: ro in CComp(ro) by Th4; o in dom ((the Sorts of A) * the ResultSort of S) by A4,PBOOLE:def 3; then A6: ((the Sorts of A) * the ResultSort of S).o = (the Sorts of A).((the ResultSort of S).o) by FUNCT_1:22 .= (the Sorts of A).ro by MSUALG_1:def 7; o in dom ((OSClass R) * the ResultSort of S) by A4,PBOOLE:def 3; then A7: ((OSClass R) * the ResultSort of S).o = (OSClass R).((the ResultSort of S).o) by FUNCT_1:22 .= (OSClass R).ro by MSUALG_1:def 7; then A8: dom (OSQuotRes(R,o)) = (the Sorts of A).ro & rng (OSQuotRes(R,o)) c= (OSClass R).ro by A6,FUNCT_2:def 1; A9: Result(o,A) = (the Sorts of A).ro by A6,MSUALG_1:def 10; then OSQuotRes(R,o).(Den(o,A).a) in rng (OSQuotRes(R,o)) by A8,FUNCT_1:def 5; then A10: OSQuotRes(R,o).(Den(o,A).a) in (OSClass R).ro by A7; A11: dom (OSQuotRes(R,o) * Den(o,A)) = dom Den(o,A) by A3,A8,A9,RELAT_1:46; hence y in Cr by A3,A7,A10,FUNCT_1:22; let b be Element of Args(o,A); assume A12: x = R #_os b; reconsider da = (Den(o,A)).a, db = (Den(o,A)).b as Element of (the Sorts of A).ro by A6,MSUALG_1:def 10; A13: da in (the Sorts of A)-carrier_of CComp(ro) by Th6; A14: y = (OSQuotRes(R,o)).((Den(o,A)).a) by A3,A11,FUNCT_1:22 .= OSClass(R, da) by Def16 .= Class( CompClass(R, CComp(ro)), da) by Def14; A15: ((OSQuotRes(R,o)) * (Den(o,A))).b = (OSQuotRes(R,o)).db by A3,A11,FUNCT_1:22 .= OSClass(R,db) by Def16 .= Class( CompClass(R, CComp(ro)), db) by Def14; for n be Nat st n in dom a holds [a.n,b.n] in R.((ar)/.n) proof let n be Nat; assume A16: n in dom a; A17: dom a = dom ar & dom b = dom ar by MSUALG_3:6; then consider ya being Element of (the Sorts of A).((ar)/.n) such that A18: ya = a.n & (R #_os a).n = OSClass(R, ya) by A16,Def15; consider yb being Element of (the Sorts of A).((ar)/.n) such that A19: yb = b.n & (R #_os b).n = OSClass(R, yb) by A16,A17,Def15; thus thesis by A2,A12,A18,A19,Th13; end; then [da,db] in R.ro by MSUALG_4:def 6; then [da,db] in CompClass(R, CComp(ro)) by A5,Def11; hence y = ((OSQuotRes(R,o)) * (Den(o,A))).b by A13,A14,A15,EQREL_1:44; end; consider f be Function such that A20: dom f = Ca & rng f c= Cr & for x be set st x in Ca holds P[x,f.x] from NonUniqBoundFuncEx(A1); reconsider f as Function of ((OSClass R)# * the Arity of S).o, ((OSClass R) * the ResultSort of S).o by A20,FUNCT_2:4; take f; thus thesis by A20; end; uniqueness proof let F,G be Function of ((OSClass R)# * the Arity of S).o, ((OSClass R) * the ResultSort of S).o; assume that A21: for a be Element of Args(o,A) st R #_os a in ((OSClass R)# * the Arity of S).o holds F.(R #_os a) = ((OSQuotRes(R,o)) * (Den(o,A))).a and A22: for a be Element of Args(o,A) st R #_os a in ((OSClass R)# * the Arity of S).o holds G.(R #_os a) = ((OSQuotRes(R,o)) * (Den(o,A))).a; set ao = the_arity_of o; A23: dom (the Arity of S) = the OperSymbols of S & rng (the Arity of S) c= (the carrier of S)* by FUNCT_2:def 1; then dom ((OSClass R)# * the Arity of S) = dom (the Arity of S) by PBOOLE:def 3; then A24: ((OSClass R)# * the Arity of S).o = (OSClass R)#.((the Arity of S).o) by A23,FUNCT_1:22 .= (OSClass R)#.ao by MSUALG_1:def 6; then A25: dom F = (OSClass R)#.ao & dom G = (OSClass R)#.ao by FUNCT_2:def 1; now let x be set; assume A26: x in (OSClass R)#.ao; then consider a be Element of Args(o,A) such that A27: x = R #_os a by A24,Th15; F.x = (OSQuotRes(R,o) * Den(o,A)).a & G.x = ((OSQuotRes(R,o)) * Den(o,A)).a by A21,A22,A24,A26,A27; hence F.x = G.x; end; hence thesis by A25,FUNCT_1:9; end; end; definition let S; let A be non-empty OSAlgebra of S; let R be OSCongruence of A; func OSQuotCharact R -> ManySortedFunction of (OSClass R)# * the Arity of S, (OSClass R) * the ResultSort of S means :Def21: for o be OperSymbol of S holds it.o = OSQuotCharact(R,o); existence proof set O = the OperSymbols of S; defpred P[set,set] means for o be OperSymbol of S st o = $1 holds $2 = OSQuotCharact(R,o); A1: for x be set st x in O ex y be set st P[x,y] proof let x be set; assume x in O; then reconsider x1 = x as OperSymbol of S; take OSQuotCharact(R,x1); thus thesis; end; consider f be Function such that A2: dom f = O & for x be set st x in O holds P[x,f.x] from NonUniqFuncEx(A1); reconsider f as ManySortedSet of O by A2,PBOOLE:def 3; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider x1 = x as OperSymbol of S by A2; f.x1 = OSQuotCharact(R,x1) by A2; hence thesis; end; then reconsider f as ManySortedFunction of O by PRALG_1:def 15; for i be set st i in O holds f.i is Function of ((OSClass R)# * the Arity of S).i, ((OSClass R) * the ResultSort of S).i proof let i be set; assume i in O; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotCharact(R,i1) by A2; hence thesis; end; then reconsider f as ManySortedFunction of ((OSClass R)# * the Arity of S), ((OSClass R) * the ResultSort of S) by MSUALG_1:def 2; take f; thus thesis by A2; end; uniqueness proof let f,g be ManySortedFunction of ((OSClass R)# * the Arity of S), ((OSClass R) * the ResultSort of S); assume that A3: for o being OperSymbol of S holds f.o = OSQuotCharact(R,o) and A4: for o being OperSymbol of S holds g.o = OSQuotCharact(R,o); now let i be set; assume i in the OperSymbols of S; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotCharact(R,i1) & g.i1 = OSQuotCharact(R,i1) by A3,A4; hence f.i = g.i; end; hence thesis by PBOOLE:3; end; end; definition let S; let U1 be non-empty OSAlgebra of S; let R be OSCongruence of U1; func QuotOSAlg(U1,R) -> OSAlgebra of S equals :Def22: MSAlgebra(# OSClass R, OSQuotCharact R #); coherence by OSALG_1:17; end; :: we could note that for discrete the QuotOSAlg and QuotMsAlg are equal definition let S; let U1 be non-empty OSAlgebra of S; let R be OSCongruence of U1; cluster QuotOSAlg (U1,R) -> strict non-empty; coherence proof QuotOSAlg (U1,R) = MSAlgebra(# OSClass R, OSQuotCharact R #) by Def22; hence thesis by MSUALG_1:def 8; end; end; definition let S; let U1 be non-empty OSAlgebra of S; let R be OSCongruence of U1; let s be Element of S; func OSNat_Hom(U1,R,s) -> Function of (the Sorts of U1).s,OSClass(R,s) means :Def23: for x being Element of (the Sorts of U1).s holds it.x = OSClass(R,x); existence proof deffunc F(Element of (the Sorts of U1).s) = OSClass(R,$1); thus ex F being Function of (the Sorts of U1).s,OSClass(R,s) st for x being Element of (the Sorts of U1).s holds F.x = F(x) from LambdaD; end; uniqueness proof let f,g be Function of (the Sorts of U1).s,OSClass (R,s); assume that A1: for x being Element of (the Sorts of U1).s holds f.x = OSClass(R,x) and A2: for x being Element of (the Sorts of U1).s holds g.x = OSClass(R,x); A3: dom f = (the Sorts of U1).s & dom g = (the Sorts of U1).s by FUNCT_2:def 1; now let x be set; assume x in (the Sorts of U1).s; then reconsider x1 = x as Element of (the Sorts of U1).s; f.x = OSClass(R,x1) & g.x = OSClass(R,x1) by A1,A2; hence f.x = g.x; end; hence thesis by A3,FUNCT_1:9; end; end; definition let S; let U1 be non-empty OSAlgebra of S; let R be OSCongruence of U1; func OSNat_Hom(U1,R) -> ManySortedFunction of U1, QuotOSAlg (U1,R) means :Def24: for s be Element of S holds it.s = OSNat_Hom(U1,R,s); existence proof deffunc F(Element of S) = OSNat_Hom(U1,R,$1); consider f be Function such that A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d) from LambdaB; reconsider f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider y = x as Element of S by A1; f.y = OSNat_Hom(U1,R,y) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the carrier of S by PRALG_1:def 15; for i be set st i in the carrier of S holds f.i is Function of (the Sorts of U1).i, (OSClass R).i proof let i be set; assume i in the carrier of S; then reconsider s = i as Element of S; A2: OSClass(R,s) = (OSClass R).i by Def13; f.s = OSNat_Hom(U1,R,s) by A1; hence thesis by A2; end; then reconsider f as ManySortedFunction of the Sorts of U1,OSClass R by MSUALG_1:def 2; QuotOSAlg (U1,R) = MSAlgebra(#OSClass R, OSQuotCharact R#) by Def22; then reconsider f as ManySortedFunction of U1,QuotOSAlg (U1,R); take f; thus thesis by A1; end; uniqueness proof let F,G be ManySortedFunction of U1, QuotOSAlg (U1,R); assume that A3: for s be Element of S holds F.s = OSNat_Hom(U1,R,s) and A4: for s be Element of S holds G.s = OSNat_Hom(U1,R,s); now let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; F.s = OSNat_Hom(U1,R,s) & G.s = OSNat_Hom(U1,R,s) by A3,A4; hence F.i = G.i; end; hence thesis by PBOOLE:3; end; end; theorem for U1 be non-empty OSAlgebra of S, R be OSCongruence of U1 holds OSNat_Hom(U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom(U1,R) is order-sorted proof let U1 be non-empty OSAlgebra of S, R be OSCongruence of U1; set F = OSNat_Hom(U1,R), QA = QuotOSAlg (U1,R), S1 = the Sorts of U1; A1: QA = MSAlgebra (# OSClass R, OSQuotCharact R #) by Def22; for o be Element of the OperSymbols of S st Args (o,U1) <> {} for x be Element of Args(o,U1) holds (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,QA).(F#x) proof let o be Element of the OperSymbols of S such that Args (o,U1) <> {}; let x be Element of Args(o,U1); set ro = the_result_sort_of o, ar = the_arity_of o; A2: Den(o,QA) = (OSQuotCharact R).o by A1,MSUALG_1:def 11 .= OSQuotCharact(R,o) by Def21; A3: dom (F#x) = dom ar & dom x = dom ar by MSUALG_3:6; A4: dom (R #_os x) = dom ((OSClass R) * (the_arity_of o)) by CARD_3:18; dom (OSClass R) = the carrier of S by PBOOLE:def 3; then rng ar c= dom (OSClass R); then A5: dom (R #_os x) = dom ar by A4,RELAT_1:46; (the Arity of S).o = ar by MSUALG_1:def 6; then A6: ((OSClass R)# * the Arity of S).o = product ((OSClass R) * ar) by MSAFREE:1; for a be set st a in dom ar holds (F#x).a = (R #_os x).a proof let a be set; assume A7: a in dom ar; then reconsider n = a as Nat; set Fo = OSNat_Hom(U1,R,((ar)/.n)), s = ((ar)/.n); A8: n in dom ((the Sorts of U1) * ar) by A7,PBOOLE:def 3; then ((the Sorts of U1) * ar).n = (the Sorts of U1).(ar.n) by FUNCT_1:22 .= S1.s by A7,FINSEQ_4:def 4; then reconsider xn = x.n as Element of S1.s by A8,MSUALG_3:6; consider z being Element of S1.s such that A9: z = x.n & (R #_os x).n = OSClass(R,z) by A7,Def15; thus (F#x).a = (F.((ar)/.n)).(x.n) by A3,A7,MSUALG_3:def 8 .= Fo.xn by Def24 .= (R #_os x).a by A9,Def23; end; then A10: F # x = R #_os x by A3,A5,FUNCT_1:9; A11: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1) by FUNCT_2:def 1; A12: dom (the Sorts of U1) = the carrier of S by PBOOLE:def 3; A13: dom (the ResultSort of S) = the OperSymbols of S & rng (the ResultSort of S) c= the carrier of S by FUNCT_2:def 1; rng (the ResultSort of S) c= dom (the Sorts of U1) by A12; then dom ((the Sorts of U1) * the ResultSort of S) = dom (the ResultSort of S) by RELAT_1:46; then A14: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the ResultSort of S).o) by A13,FUNCT_1:22 .= (the Sorts of U1).ro by MSUALG_1:def 7; then A15: Result(o,U1) = S1.ro by MSUALG_1:def 10; reconsider dx = (Den(o,U1)).x as Element of S1.ro by A14,MSUALG_1:def 10; rng Den(o,U1) c= dom OSQuotRes(R,o) by A11,A14,A15,FUNCT_2:def 1; then A16: dom ((OSQuotRes(R,o)) * Den(o,U1)) = dom Den(o,U1) by RELAT_1:46; Den(o,QA).(F#x) = ((OSQuotRes(R,o)) * (Den(o,U1))).x by A2,A6,A10,Def20 .= (OSQuotRes(R,o)) . dx by A11,A16,FUNCT_1:22 .= OSClass (R, dx) by Def16 .= (OSNat_Hom(U1,R,ro)).dx by Def23 .= (F.ro).((Den(o,U1)).x) by Def24; hence thesis; end; hence F is_homomorphism U1,QA by MSUALG_3:def 9; for i be set st i in the carrier of S holds rng (F.i) = (the Sorts of QA).i proof let i be set; assume i in the carrier of S; then reconsider s = i as Element of S; reconsider f = F.i as Function of S1.s, (the Sorts of QA).s by MSUALG_1:def 2; QA = MSAlgebra (# OSClass R,OSQuotCharact R #) by Def22; then A17: (the Sorts of QA).s = OSClass (R,s) by Def13; A18: dom f = S1.s & rng f c= (the Sorts of QA).s by FUNCT_2:def 1; for x be set st x in (the Sorts of QA).i holds x in rng f proof let x be set; assume x in (the Sorts of QA).i; then consider a1 being set such that A19: a1 in S1.s & x = Class(CompClass(R,CComp(s)),a1) by A17,Def12; reconsider a2 = a1 as Element of S1.s by A19; A20: OSClass(R,a2) = x by A19,Def14; A21: f.a1 in rng f by A18,A19,FUNCT_1:def 5; f = OSNat_Hom(U1,R,s) by Def24; hence thesis by A20,A21,Def23; end; then (the Sorts of QA).i c= rng f by TARSKI:def 3; hence thesis by XBOOLE_0:def 10; end; hence F is "onto" by MSUALG_3:def 3; thus F is order-sorted proof let s1,s2 be Element of S such that A22: s1 <= s2; let a1 be set such that A23: a1 in dom (F.s1); reconsider S2 = S1 as OrderSortedSet of S by OSALG_1:17; A24: S2.s1 c= S2.s2 by A22,OSALG_1:def 18; A25: dom (F.s2) = S1.s2 by FUNCT_2:def 1; A26: a1 in S1.s1 by A23; hence a1 in dom (F.s2) by A24,A25; reconsider b1 = a1 as Element of S1.s1 by A23; reconsider b2 = a1 as Element of S1.s2 by A24,A26; thus (F.s1).a1 = OSNat_Hom(U1,R,s1).b1 by Def24 .= OSClass(R,b1) by Def23 .= OSClass(R,b2) by A22,Th14 .= OSNat_Hom(U1,R,s2).b2 by Def23 .= (F.s2).a1 by Def24; end; end; theorem Th17: for U1,U2 being non-empty OSAlgebra of S, F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds MSCng(F) is OSCongruence of U1 proof let U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2 such that A1: F is_homomorphism U1,U2 & F is order-sorted; reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; MSCng(F) is os-compatible proof let s1,s2 be Element of S such that A2: s1 <= s2; reconsider s3 = s1, s4 = s2 as SortSymbol of S; let x,y be set such that A3: x in (the Sorts of U1).s1 & y in (the Sorts of U1).s1; A4: S1.s3 c= S1.s4 by A2,OSALG_1:def 18; A5: dom (F.s3) = S1.s3 & dom (F.s4) = S1.s4 by FUNCT_2:def 1; reconsider x1 = x, y1 = y as Element of (the Sorts of U1).s1 by A3; reconsider x2 = x, y2 = y as Element of (the Sorts of U1).s2 by A3,A4; A6: [x2,y2] in MSCng(F,s2) iff (F.s2).x2 = (F.s2).y2 by MSUALG_4:def 19; A7: x1 in dom (F.s4) & (F.s3).x1 = (F.s4).x1 & y1 in dom (F.s4) & (F.s3).y1 = (F.s4).y1 by A1,A2,A5,OSALG_3:def 1; (MSCng(F)).s1 = MSCng(F,s1) & (MSCng(F)).s2 = MSCng(F,s2) by A1,MSUALG_4:def 20; hence [x,y] in (MSCng(F)).s1 iff [x,y] in (MSCng(F)).s2 by A6,A7,MSUALG_4: def 19; end; hence MSCng(F) is OSCongruence of U1 by Def3; end; :: just a casting func, currently no other way how to employ the type system definition let S; let U1,U2 be non-empty OSAlgebra of S; let F be ManySortedFunction of U1,U2; assume A1: F is_homomorphism U1,U2 & F is order-sorted; func OSCng(F) -> OSCongruence of U1 equals :Def25: MSCng(F); correctness by A1,Th17; end; definition let S; let U1,U2 be non-empty OSAlgebra of S; let F be ManySortedFunction of U1,U2; let s be Element of S; assume A1: F is_homomorphism U1,U2 & F is order-sorted; func OSHomQuot(F,s) -> Function of (the Sorts of (QuotOSAlg (U1,OSCng F))).s,(the Sorts of U2).s means:Def26: for x be Element of (the Sorts of U1).s holds it.(OSClass(OSCng(F),x)) = (F.s).x; existence proof set qa = QuotOSAlg (U1,OSCng F), cqa = the Sorts of qa, S1 = the Sorts of U1, S2 = the Sorts of U2; qa = MSAlgebra (# OSClass OSCng(F),OSQuotCharact OSCng(F) #) by Def22; then A2: cqa.s = OSClass (OSCng(F),s) by Def13; defpred P[set,set] means for a be Element of S1.s st $1 = OSClass(OSCng(F),a) holds $2 = (F.s).a; A3: for x be set st x in cqa.s ex y be set st y in S2.s & P[x,y] proof let x be set; assume x in cqa.s; then consider a being set such that A4: a in (the Sorts of U1).s & x = Class( CompClass(OSCng(F),CComp(s)), a) by A2,Def12; reconsider a as Element of S1.s by A4; take y = (F.s).a; thus y in S2.s; A5: x = OSClass(OSCng(F),a) by A4,Def14; let b be Element of S1.s; assume x = OSClass(OSCng(F),b); then [b,a] in (OSCng(F)).s by A5,Th13; then [b,a] in (MSCng(F)).s by A1,Def25; then [b,a] in MSCng(F,s) by A1,MSUALG_4:def 20; hence thesis by MSUALG_4:def 19; end; consider G being Function such that A6: dom G = cqa.s & rng G c= S2.s & for x be set st x in cqa.s holds P[x,G.x] from NonUniqBoundFuncEx(A3); reconsider G as Function of cqa.s,S2.s by A6,FUNCT_2:def 1,RELSET_1:11; take G; let a be Element of S1.s; thus G.(OSClass(OSCng(F),a)) = (F.s).a by A2,A6; end; uniqueness proof set qa = QuotOSAlg (U1, OSCng F), cqa = the Sorts of qa, u1 = the Sorts of U1, u2 = the Sorts of U2; qa = MSAlgebra (# OSClass OSCng(F),OSQuotCharact OSCng(F) #) by Def22; then A7: cqa.s = OSClass (OSCng(F),s) by Def13; let H,G be Function of cqa.s,u2.s; assume that A8: for a be Element of u1.s holds H.(OSClass(OSCng(F),a)) = (F.s).a and A9: for a be Element of u1.s holds G.(OSClass(OSCng(F),a)) = (F.s).a; for x be set st x in cqa.s holds H.x = G.x proof let x be set; assume x in cqa.s; then consider y being set such that A10: y in (the Sorts of U1).s & x = Class( CompClass(OSCng(F),CComp(s)), y) by A7,Def12; reconsider y1 = y as Element of u1.s by A10; A11: OSClass(OSCng(F),y1) = x by A10,Def14; hence H.x = (F.s).y1 by A8 .= G.x by A9,A11; end; hence thesis by FUNCT_2:18; end; end; :: this seems a bit too permissive, but same as the original :: we should assume F order-sorted probably definition let S; let U1,U2 be non-empty OSAlgebra of S; let F be ManySortedFunction of U1,U2; func OSHomQuot(F) -> ManySortedFunction of (QuotOSAlg (U1, OSCng F)),U2 means :Def27: for s be Element of S holds it.s = OSHomQuot(F,s); existence proof deffunc F(Element of S) = OSHomQuot(F,$1); consider f be Function such that A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d) from LambdaB; reconsider f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider y = x as Element of S by A1; f.y = OSHomQuot(F,y) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the carrier of S by PRALG_1:def 15; for i be set st i in the carrier of S holds f.i is Function of (the Sorts of QuotOSAlg (U1, OSCng F)).i, (the Sorts of U2).i proof let i be set; assume i in the carrier of S; then reconsider s = i as Element of S; f.s = OSHomQuot(F,s) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the Sorts of QuotOSAlg (U1,OSCng F),the Sorts of U2 by MSUALG_1:def 2; reconsider f as ManySortedFunction of QuotOSAlg (U1,OSCng F),U2; take f; thus thesis by A1; end; uniqueness proof let H,G be ManySortedFunction of QuotOSAlg (U1,OSCng F),U2; assume that A2: for s be Element of S holds H.s = OSHomQuot(F,s) and A3: for s be Element of S holds G.s = OSHomQuot(F,s); now let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; H.s = OSHomQuot(F,s) & G.s = OSHomQuot(F,s) by A2,A3; hence H.i = G.i; end; hence thesis by PBOOLE:3; end; end; theorem Th18: for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSHomQuot(F) is_monomorphism QuotOSAlg (U1,OSCng F),U2 & OSHomQuot(F) is order-sorted proof let U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2; set mc = OSCng(F), qa = QuotOSAlg (U1,mc), qh = OSHomQuot(F), S1 = the Sorts of U1; assume A1: F is_homomorphism U1,U2 & F is order-sorted; A2: qa = MSAlgebra (# OSClass mc, OSQuotCharact mc #) by Def22; for o be Element of the OperSymbols of S st Args (o,qa) <> {} for x be Element of Args(o,qa) holds (qh.(the_result_sort_of o)).(Den(o,qa).x) = Den(o,U2).(qh#x) proof let o be Element of the OperSymbols of S such that Args (o,qa) <> {}; let x be Element of Args(o,qa); reconsider o1 = o as OperSymbol of S; set ro = the_result_sort_of o, ar = the_arity_of o; A3: Den(o,qa) = (OSQuotCharact mc).o by A2,MSUALG_1:def 11 .= OSQuotCharact(mc,o1) by Def21; Args(o,qa) = ((OSClass mc)# * (the Arity of S)).o by A2,MSUALG_1:def 9; then consider a be Element of Args(o,U1) such that A4: x = mc #_os a by Th15; A5: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1) by FUNCT_2:def 1; o in the OperSymbols of S; then o in dom (S1 * the ResultSort of S) by PBOOLE:def 3; then A6: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the ResultSort of S).o) by FUNCT_1:22 .= (the Sorts of U1).ro by MSUALG_1:def 7; then A7: Result(o,U1) = S1.ro by MSUALG_1:def 10; reconsider da = (Den(o,U1)).a as Element of S1.ro by A6,MSUALG_1:def 10; A8: qh.ro = OSHomQuot(F,ro) by Def27; rng Den(o,U1) c= dom OSQuotRes(mc,o) by A5,A6,A7,FUNCT_2:def 1; then A9: dom ((OSQuotRes(mc,o)) * Den(o,U1)) = dom Den(o,U1) by RELAT_1:46; A10: dom (qh # x) = dom ar & dom (F # a) = dom ar & dom x = dom ar & dom a = dom ar by MSUALG_3:6; A11: now let y be set; assume A12: y in dom ar; then reconsider n = y as Nat; A13: ar/.n = ar.n by A12,FINSEQ_4:def 4; ar.n in rng ar by A12,FUNCT_1:def 5; then reconsider s = ar.n as SortSymbol of S; consider an being Element of S1.s such that A14: an = a.n & x.n = OSClass(mc,an) by A4,A12,A13,Def15; (qh # x).n = (qh.s).(x.n) by A10,A12,A13,MSUALG_3:def 8 .= OSHomQuot(F,s).OSClass(mc,an) by A14,Def27 .= (F.s).an by A1,Def26 .= (F # a).n by A10,A12,A13,A14,MSUALG_3:def 8; hence (qh # x).y = (F # a).y; end; ar = (the Arity of S).o by MSUALG_1:def 6; then product((OSClass mc) * ar) = ((OSClass mc)# * the Arity of S).o by MSAFREE:1; then Den(o,qa).x = (OSQuotRes(mc,o) * Den(o,U1)).a by A3,A4,Def20 .= (OSQuotRes(mc,o)) . da by A5,A9,FUNCT_1:22 .= OSClass (OSCng(F),da) by Def16; then (qh.ro).(Den(o,qa).x) = (F.ro).((Den(o,U1)).a) by A1,A8,Def26 .= Den(o,U2).(F#a) by A1,MSUALG_3:def 9; hence thesis by A10,A11,FUNCT_1:9; end; hence qh is_homomorphism qa,U2 by MSUALG_3:def 9; for i be set st i in the carrier of S holds (qh.i) is one-to-one proof let i be set; set f = qh.i; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A15: f = OSHomQuot(F,s) by Def27; for x1,x2 be set st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2 proof let x1,x2 be set; assume A16: x1 in dom f & x2 in dom f & f.x1 = f.x2; then x1 in (OSClass mc).s & x2 in (OSClass mc).s by A2,A15,FUNCT_2:def 1; then A17: x1 in OSClass (mc,s) & x2 in OSClass (mc,s) by Def13; then consider a1 being set such that A18: a1 in S1.s & x1 = Class( CompClass(OSCng(F),CComp(s)), a1) by Def12; consider a2 being set such that A19: a2 in S1.s & x2 = Class( CompClass(OSCng(F),CComp(s)), a2) by A17,Def12; reconsider a1 as Element of S1.s by A18; reconsider a2 as Element of S1.s by A19; A20: x1 = OSClass(OSCng(F),a1) & x2 = OSClass(OSCng(F),a2) by A18,A19,Def14; (F.s).a1 = f.(OSClass(OSCng(F),a1)) & (F.s).a2 = f.(OSClass(OSCng(F),a2)) by A1,A15,Def26; then [a1,a2] in MSCng(F,s) by A16,A20,MSUALG_4:def 19; then [a1,a2] in (MSCng(F)).s by A1,MSUALG_4:def 20; then [a1,a2] in (OSCng(F)).s by A1,Def25; hence thesis by A20,Th13; end; hence thesis by FUNCT_1:def 8; end; hence qh is "1-1" by MSUALG_3:1; thus OSHomQuot(F) is order-sorted proof let s1,s2 being Element of S such that A21: s1 <= s2; let a1 be set such that A22: a1 in dom (qh.s1); reconsider sqa = the Sorts of qa as OrderSortedSet of S by OSALG_1:17; reconsider S1O = S1 as OrderSortedSet of S by OSALG_1:17; A23: S1O.s1 c= S1O.s2 by A21,OSALG_1:def 18; A24: dom (qh.s1) = (the Sorts of qa).s1 & dom (qh.s2) = (the Sorts of qa).s2 by FUNCT_2:def 1; sqa.s1 c= sqa.s2 by A21,OSALG_1:def 18; hence a1 in dom (qh.s2) by A22,A24; qa = MSAlgebra(# OSClass mc, OSQuotCharact mc #) by Def22; then a1 in (OSClass OSCng(F)).s1 by A22; then a1 in OSClass (OSCng(F),s1) by Def13; then consider x being set such that A25: x in S1.s1 and A26: a1 = Class( CompClass(OSCng(F),CComp(s1)), x) by Def12; reconsider x1 = x as Element of S1.s1 by A25; reconsider x2 = x as Element of S1.s2 by A23,A25; reconsider s3 = s1, s4 = s2 as Element of S; x1 in dom (F.s3) by A25,FUNCT_2:def 1; then A27: x1 in dom (F.s4) & (F.s3).x1 = (F.s4).x1 by A1,A21,OSALG_3:def 1; A28: a1 = OSClass(OSCng(F),x1) by A26,Def14; then A29: a1 = OSClass(OSCng(F),x2) by A21,Th14; thus (qh.s1).a1 = OSHomQuot(F,s1).(OSClass(OSCng(F),x1)) by A28,Def27 .= (F.s2).x1 by A1,A27,Def26 .= OSHomQuot(F,s2).(OSClass(OSCng(F),x2)) by A1,Def26 .= (qh.s2).a1 by A29,Def27; end; end; theorem Th19: for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds OSHomQuot(F) is_isomorphism QuotOSAlg (U1,OSCng F),U2 proof let U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2; set mc = OSCng(F), qa = QuotOSAlg (U1,mc), qh = OSHomQuot(F); assume A1: F is_epimorphism U1,U2 & F is order-sorted; then A2: F is_homomorphism U1,U2 & F is "onto" by MSUALG_3:def 10; then qh is_monomorphism qa,U2 by A1,Th18; then A3: qh is_homomorphism qa,U2 & qh is "1-1" by MSUALG_3:def 11; set Sq = the Sorts of qa, S1 = the Sorts of U1, S2 = the Sorts of U2; for i be set st i in the carrier of S holds rng (qh.i) = S2.i proof let i be set; set f = qh.i; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; A4: qh.i = OSHomQuot(F,s) by Def27; then A5: dom f = Sq.s & rng f c= S2.s by FUNCT_2:def 1,RELSET_1:12; thus rng f c= S2.i by A4,RELSET_1:12; A6: rng (F.s) = S2.s by A2,MSUALG_3:def 3; let x be set; assume x in S2.i; then consider a be set such that A7: a in dom (F.s) & (F.s).a = x by A6,FUNCT_1:def 5; reconsider a as Element of S1.s by A7; A8: f.(OSClass(OSCng(F),a)) = x by A1,A2,A4,A7,Def26; qa = MSAlgebra(#OSClass OSCng(F),OSQuotCharact OSCng(F)#) by Def22; then Sq.s = OSClass (OSCng(F),s) by Def13; hence thesis by A5,A8,FUNCT_1:def 5; end; then qh is "onto" by MSUALG_3:def 3; hence thesis by A3,MSUALG_3:13; end; theorem for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds QuotOSAlg (U1,OSCng F),U2 are_isomorphic proof let U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2; assume F is_epimorphism U1,U2 & F is order-sorted; then OSHomQuot(F) is_isomorphism QuotOSAlg (U1,OSCng F),U2 by Th19; hence thesis by MSUALG_3:def 13; end; :: monotone OSCongruence ... monotonicity is properly stronger :: than MSCongruence, so we define it more broadly and prove the :: ccluster then, however if used for other things than OSCongruences :: the name of the attribute should be changed :: this condition is nontrivial only for nonmonotone osas (see further), :: where Den(o1,U1).x1 can differ from Den(o2,U2).x1 :: is OK for constants ... their Args is always {{}}, so o1 <= o2 :: implies for them [Den(o1,U1).{},Den(o2,U1).{}] in R definition let S be OrderSortedSign, U1 be non-empty OSAlgebra of S, R be MSEquivalence-like OrderSortedRelation of U1; attr R is monotone means :Def28: for o1,o2 being OperSymbol of S st o1 <= o2 for x1 being Element of Args(o1,U1) for x2 being Element of Args(o2,U1) st ( for y being Nat st y in dom x1 holds [x1.y,x2.y] in R.((the_arity_of o2)/.y) ) holds [Den(o1,U1).x1,Den(o2,U1).x2] in R.(the_result_sort_of o2); end; theorem Th21: for S being OrderSortedSign, U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1 |] is OSCongruence of U1 proof let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; reconsider C = [| the Sorts of U1, the Sorts of U1 |] as MSCongruence of U1 by MSUALG_5:20; C is os-compatible proof let s1,s2 be Element of S such that A1: s1 <= s2; reconsider s3 = s1, s4 = s2 as Element of S; let x,y be set such that A2: x in (the Sorts of U1).s1 & y in (the Sorts of U1).s1; reconsider O1 = (the Sorts of U1) as OrderSortedSet of S by OSALG_1:17; A3: O1.s3 c= O1.s4 by A1,OSALG_1:def 18; C.s1 = [:(the Sorts of U1).s1,(the Sorts of U1).s1:] & C.s2 = [:(the Sorts of U1).s2,(the Sorts of U1).s2:] by PRALG_2:def 9; hence [x,y] in C.s1 iff [x,y] in C.s2 by A2,A3,ZFMISC_1:106; end; hence [| the Sorts of U1, the Sorts of U1 |] is OSCongruence of U1 by Def3; end; theorem Th22: for S being OrderSortedSign, U1 being non-empty OSAlgebra of S, R being OSCongruence of U1 st R = [| (the Sorts of U1), (the Sorts of U1) |] holds R is monotone proof let S be OrderSortedSign, U1 be non-empty OSAlgebra of S, R be OSCongruence of U1 such that A1: R = [| (the Sorts of U1), (the Sorts of U1) |]; let o1,o2 be OperSymbol of S such that A2: o1 <= o2; let x1 be Element of Args(o1,U1); let x2 be Element of Args(o2,U1) such that for y being Nat st y in dom x1 holds [x1.y,x2.y] in R.((the_arity_of o2)/.y); set s2 = the_result_sort_of o2, s1 = the_result_sort_of o1; A3: s1 <= s2 by A2,OSALG_1:def 22; reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; A4: O1.s1 c= O1.s2 by A3,OSALG_1:def 18; Den(o1,U1).x1 in (the Sorts of U1).s1 by MSUALG_9:19; then A5: Den(o1,U1).x1 in (the Sorts of U1).s2 & Den(o2,U1).x2 in (the Sorts of U1).s2 by A4,MSUALG_9:19; R.s2 = [:(the Sorts of U1).s2,(the Sorts of U1).s2:] by A1,PRALG_2:def 9; hence [Den(o1,U1).x1,Den(o2,U1).x2] in R.(the_result_sort_of o2) by A5,ZFMISC_1:106; end; definition let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster monotone OSCongruence of U1; existence proof reconsider R = [| the Sorts of U1, the Sorts of U1 |] as OSCongruence of U1 by Th21; take R; thus thesis by Th22; end; end; definition let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster monotone (MSEquivalence-like OrderSortedRelation of U1); existence proof consider R being monotone OSCongruence of U1; take R; thus thesis; end; end; theorem Th23: for S being OrderSortedSign, U1 being non-empty OSAlgebra of S, R being monotone (MSEquivalence-like OrderSortedRelation of U1) holds R is MSCongruence-like proof let S be OrderSortedSign, U1 be non-empty OSAlgebra of S, R be monotone (MSEquivalence-like OrderSortedRelation of U1); for o be (Element of the OperSymbols of S), x,y be Element of Args(o,U1) st (for n be Nat st n in dom x holds [x.n,y.n] in R.((the_arity_of o)/.n)) holds [Den(o,U1).x,Den(o,U1).y] in R.(the_result_sort_of o) by Def28; hence R is MSCongruence-like by MSUALG_4:def 6; end; definition let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster monotone -> MSCongruence-like (MSEquivalence-like OrderSortedRelation of U1); coherence by Th23; end; theorem Th24: for S being OrderSortedSign, U1 being monotone non-empty OSAlgebra of S, R being OSCongruence of U1 holds R is monotone proof let S be OrderSortedSign, U1 be monotone non-empty OSAlgebra of S, R be OSCongruence of U1; let o1,o2 be OperSymbol of S such that A1: o1 <= o2; let x1 be Element of Args(o1,U1); let x2 be Element of Args(o2,U1) such that A2: for y being Nat st y in dom x1 holds [x1.y,x2.y] in R.((the_arity_of o2)/.y); A3: Den(o1,U1) c= Den(o2,U1) by A1,OSALG_1:27; Args(o1,U1) c= Args(o2,U1) by A1,OSALG_1:26; then reconsider x3 = x1 as Element of Args(o2,U1) by TARSKI:def 3; A4: [Den(o2,U1).x3,Den(o2,U1).x2] in R.(the_result_sort_of o2) by A2,MSUALG_4:def 6; x1 in Args(o1,U1); then x1 in dom Den(o1,U1) by FUNCT_2:def 1; hence [Den(o1,U1).x1,Den(o2,U1).x2] in R.(the_result_sort_of o2) by A3,A4, GRFUNC_1:8; end; definition let S be OrderSortedSign, U1 be monotone non-empty OSAlgebra of S; cluster -> monotone OSCongruence of U1; coherence by Th24; end; :: monotonicity of quotient by monotone oscongruence definition let S; let U1 be non-empty OSAlgebra of S; let R be monotone OSCongruence of U1; cluster QuotOSAlg(U1,R) -> monotone; coherence proof set A = QuotOSAlg(U1,R); A1: A = MSAlgebra(# OSClass R, OSQuotCharact R #) by Def22; reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; let o1,o2 be OperSymbol of S such that A2: o1 <= o2; A3: o1 ~= o2 & (the_arity_of o1) <= (the_arity_of o2) & the_result_sort_of o1 <= the_result_sort_of o2 by A2,OSALG_1:def 22; A4: dom Den(o2,A) = Args(o2,A) & dom Den(o1,A) = Args(o1,A) by FUNCT_2:def 1; A5: Args(o1,A) c= Args(o2,A) & Result(o1,A) c= Result(o2,A) by A2,OSALG_1:26; then A6: dom Den(o1,A) = (dom Den(o2,A)) /\ Args(o1,A) by A4,XBOOLE_1:28; Den(o1,A) = (OSQuotCharact R).o1 & Den(o2,A) = (OSQuotCharact R).o2 by A1,MSUALG_1:def 11; then A7: Den(o1,A) = OSQuotCharact( R,o1) & Den(o2,A) = OSQuotCharact( R,o2) by Def21; A8: O1.(the_result_sort_of o1) c= O1.(the_result_sort_of o2) by A3,OSALG_1:def 19; o1 in the OperSymbols of S & o2 in the OperSymbols of S; then A9: o1 in dom (the ResultSort of S) & o2 in dom (the ResultSort of S) by FUNCT_2:def 1; len (the_arity_of o1) = len (the_arity_of o2) by A3,OSALG_1:def 7; then A10: dom (the_arity_of o1) = dom (the_arity_of o2) by FINSEQ_3:31; for x being set st x in dom Den(o1,A) holds Den(o1,A).x = Den(o2,A).x proof let x be set such that A11: x in dom Den(o1,A); A12: x in Args(o1,A) by A11; then x in Args(o2,A) by A5; then A13: x in ((OSClass R)# * the Arity of S).o1 & x in ((OSClass R)# * the Arity of S).o2 by A1,A12,MSUALG_1:def 9; then consider a1 being Element of Args(o1,U1) such that A14: x = R #_os a1 by Th15; consider a2 being Element of Args(o2,U1) such that A15: x = R #_os a2 by A13,Th15; for y being Nat st y in dom a1 holds [a1.y,a2.y] in R.((the_arity_of o2)/.y) proof let y be Nat such that A16: y in dom a1; A17: y in dom (the_arity_of o1) & y in dom (the_arity_of o2) by A10,A16,MSUALG_6:2; then consider z1 being Element of (the Sorts of U1).((the_arity_of o1)/.y ) such that A18: z1 = a1.y & (R #_os a1).y = OSClass(R, z1) by Def15; consider z2 being Element of (the Sorts of U1).((the_arity_of o2)/.y) such that A19: z2 = a2.y & (R #_os a2).y = OSClass(R, z2) by A17,Def15; A20: (the_arity_of o1)/.y = (the_arity_of o1).y & (the_arity_of o2)/.y = (the_arity_of o2).y by A17,FINSEQ_4:def 4; reconsider s1 = (the_arity_of o1).y, s2 = (the_arity_of o2).y as SortSymbol of S by A17,PARTFUN1:27; A21: s1 <= s2 by A3,A17,OSALG_1:def 7; then (the Sorts of U1).((the_arity_of o1)/.y) c= (the Sorts of U1).((the_arity_of o2)/.y) by A20,OSALG_1:def 19; then reconsider z12 = z1 as Element of (the Sorts of U1).((the_arity_of o2)/.y) by TARSKI:def 3; OSClass(R, z2) = OSClass(R, z12) by A14,A15,A18,A19,A20,A21,Th14; hence [a1.y,a2.y] in R.((the_arity_of o2)/.y) by A18,A19,Th13; end; then A22: [Den(o1,U1).a1,Den(o2,U1).a2] in R.(the_result_sort_of o2) by A2,Def28; A23: OSQuotCharact(R,o1).(R #_os a1) = ((OSQuotRes(R,o1)) * (Den(o1,U1))).a1 & OSQuotCharact(R,o2).(R #_os a2) = ((OSQuotRes(R,o2)) * (Den(o2,U1))).a2 by A13,A14,A15,Def20; Result(o1,U1) = ((the Sorts of U1) * the ResultSort of S).o1 by MSUALG_1:def 10 .= (the Sorts of U1).((the ResultSort of S).o1) by A9,FUNCT_1:23 .= (the Sorts of U1).(the_result_sort_of o1) by MSUALG_1:def 7; then reconsider da1 = Den(o1,U1).a1 as Element of (the Sorts of U1).(the_result_sort_of o1); a1 in Args(o1,U1); then a1 in dom Den(o1,U1) by FUNCT_2:def 1; then A24: ((OSQuotRes(R,o1)) * (Den(o1,U1))).a1 = OSQuotRes(R,o1).da1 by FUNCT_1:23 .= OSClass(R,da1) by Def16; Result(o2,U1) = ((the Sorts of U1) * the ResultSort of S).o2 by MSUALG_1:def 10 .= (the Sorts of U1).((the ResultSort of S).o2) by A9,FUNCT_1:23 .= (the Sorts of U1).(the_result_sort_of o2) by MSUALG_1:def 7; then reconsider da2 = Den(o2,U1).a2 as Element of (the Sorts of U1).(the_result_sort_of o2); a2 in Args(o2,U1); then a2 in dom Den(o2,U1) by FUNCT_2:def 1; then A25: ((OSQuotRes(R,o2)) * (Den(o2,U1))).a2 = OSQuotRes(R,o2).da2 by FUNCT_1:23 .= OSClass(R,da2) by Def16; reconsider da12 = da1 as Element of (the Sorts of U1).(the_result_sort_of o2) by A8,TARSKI:def 3; OSClass(R,da1) = OSClass(R,da12) by A3,Th14 .= OSClass(R,da2) by A22,Th13; hence Den(o1,A).x = Den(o2,A).x by A7,A14,A15,A23,A24,A25; end; hence Den(o2,A)|Args(o1,A) = Den(o1,A) by A6,FUNCT_1:68; end; end; theorem for S ::being locally_directed OrderSortedSign, for U1 be non-empty OSAlgebra of S, R be monotone OSCongruence of U1 holds QuotOSAlg(U1,R) is monotone OSAlgebra of S; theorem for U1 being non-empty OSAlgebra of S, U2 being monotone non-empty OSAlgebra of S, F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSCng(F) is monotone proof let U1 be non-empty OSAlgebra of S, U2 be monotone non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2 such that A1: F is_homomorphism U1,U2 & F is order-sorted; set O1 = the Sorts of U1; reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; let o1,o2 being OperSymbol of S such that A2: o1 <= o2; set R = OSCng(F), w1 = the_arity_of o1, w2 = the_arity_of o2, rs1 = the_result_sort_of o1, rs2 = the_result_sort_of o2; let x1 being (Element of Args(o1,U1)), x2 being Element of Args(o2,U1) such that A3: for y being Nat st y in dom x1 holds [x1.y,x2.y] in R.((the_arity_of o2)/.y); set D1 = Den(o1,U1).x1, D2 = Den(o2,U1).x2, M = MSCng(F); A4: M.rs1 = MSCng(F,rs1) & M.rs2 = MSCng(F,rs2) & M = R by A1,Def25,MSUALG_4:def 20; A5: Args(o1,U1) c= Args(o2,U1) & Result(o1,U1) c= Result(o2,U1) by A2,OSALG_1:26; A6: w1 <= w2 & rs1 <= rs2 by A2,OSALG_1:def 22; then A7: S1.rs1 c= S1.rs2 by OSALG_1:def 18; reconsider x12=x1 as Element of Args(o2,U1) by A5,TARSKI:def 3; A8: [Den(o2,U1).x12,Den(o2,U1).x2] in R.rs2 by A3,MSUALG_4:def 6; A9: D2 in O1.rs2 & Den(o2,U1).x12 in O1.rs2 & D1 in S1.rs1 by MSUALG_9:19; then A10: D1 in S1.rs2 & D1 in dom (F.rs1) by A7,FUNCT_2:def 1; reconsider D11=D1,D12=Den(o2,U1).x12 as Element of O1.rs2 by A7,A9; F#x1 in Args(o1,U2); then A11: F#x1 in dom Den(o1,U2) by FUNCT_2:def 1; A12: Den(o2,U2)|Args(o1,U2) = Den(o1,U2) by A2,OSALG_1:def 23; (F.rs2).(Den(o1,U1).x1) = (F.rs1).(Den(o1,U1).x1) by A1,A6,A10,OSALG_3:def 1 .= Den(o1,U2).(F#x1) by A1,MSUALG_3:def 9 .= Den(o2,U2).(F#x1) by A11,A12,FUNCT_1:68 .= Den(o2,U2).(F#x12) by A1,A2,OSALG_3:13 .= (F.rs2).(Den(o2,U1).x12) by A1,MSUALG_3:def 9; then A13: [D11,D12] in MSCng(F,rs2) by MSUALG_4:def 19; field(R.rs2) = (O1.rs2) by ORDERS_1:97; then (R.rs2) is_transitive_in (O1.rs2) by RELAT_2:def 16; hence [Den(o1,U1).x1,Den(o2,U1).x2] in R.rs2 by A4,A8,A9,A13,RELAT_2:def 8; end; :: these are a bit more general versions of OSHomQuot, that :: I need for OSAFREE; more proper way how to do this is restating :: the MSUALG_9 quotient theorems for OSAs, but that's more work definition let S; let U1,U2 be non-empty OSAlgebra of S; let F be ManySortedFunction of U1,U2; let R be OSCongruence of U1; let s be Element of S; assume A1: F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F; func OSHomQuot(F,R,s) -> Function of (the Sorts of (QuotOSAlg (U1,R))).s,(the Sorts of U2).s means :Def29: for x be Element of (the Sorts of U1).s holds it.(OSClass(R,x)) = (F.s).x; existence proof set qa = QuotOSAlg (U1,R), cqa = the Sorts of qa, S1 = the Sorts of U1, S2 = the Sorts of U2; qa = MSAlgebra (# OSClass R,OSQuotCharact R #) by Def22; then A2: cqa.s = OSClass (R,s) by Def13; defpred P[set,set] means for a be Element of S1.s st $1 = OSClass(R,a) holds $2 = (F.s).a; A3: for x be set st x in cqa.s ex y be set st y in S2.s & P[x,y] proof let x be set; assume x in cqa.s; then consider a being set such that A4: a in (the Sorts of U1).s & x = Class( CompClass(R,CComp(s)), a) by A2,Def12; reconsider a as Element of S1.s by A4; take y = (F.s).a; A5: R.s c= (OSCng F).s by A1,PBOOLE:def 5; thus y in S2.s; A6: x = OSClass(R,a) by A4,Def14; let b be Element of S1.s; assume x = OSClass(R,b); then [b,a] in R.s by A6,Th13; then [b,a] in (OSCng(F)).s by A5; then [b,a] in (MSCng(F)).s by A1,Def25; then [b,a] in MSCng(F,s) by A1,MSUALG_4:def 20; hence thesis by MSUALG_4:def 19; end; consider G being Function such that A7: dom G = cqa.s & rng G c= S2.s & for x be set st x in cqa.s holds P[x,G.x] from NonUniqBoundFuncEx(A3); reconsider G as Function of cqa.s,S2.s by A7,FUNCT_2:def 1,RELSET_1:11; take G; let a be Element of S1.s; thus G.(OSClass(R,a)) = (F.s).a by A2,A7; end; uniqueness proof set qa = QuotOSAlg (U1, R), cqa = the Sorts of qa, u1 = the Sorts of U1, u2 = the Sorts of U2; qa = MSAlgebra (# OSClass R,OSQuotCharact R #) by Def22; then A8: cqa.s = OSClass (R,s) by Def13; let H,G be Function of cqa.s,u2.s; assume that A9: for a be Element of u1.s holds H.(OSClass(R,a)) = (F.s).a and A10: for a be Element of u1.s holds G.(OSClass(R,a)) = (F.s).a; for x be set st x in cqa.s holds H.x = G.x proof let x be set; assume x in cqa.s; then consider y being set such that A11: y in (the Sorts of U1).s & x = Class( CompClass(R,CComp(s)), y) by A8,Def12; reconsider y1 = y as Element of u1.s by A11; A12: OSClass(R,y1) = x by A11,Def14; hence H.x = (F.s).y1 by A9 .= G.x by A10,A12; end; hence thesis by FUNCT_2:18; end; end; :: this seems a bit too permissive, but same as the original :: we should assume F order-sorted probably definition let S; let U1,U2 be non-empty OSAlgebra of S; let F be ManySortedFunction of U1,U2; let R be OSCongruence of U1; func OSHomQuot(F,R) -> ManySortedFunction of (QuotOSAlg (U1, R)),U2 means :Def30: for s be Element of S holds it.s = OSHomQuot(F,R,s); existence proof deffunc F(Element of S) = OSHomQuot(F,R,$1); consider f be Function such that A1: dom f = the carrier of S & for d be Element of S holds f.d = F(d) from LambdaB; reconsider f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3; for x be set st x in dom f holds f.x is Function proof let x be set; assume x in dom f; then reconsider y = x as Element of S by A1; f.y = OSHomQuot(F,R,y) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the carrier of S by PRALG_1:def 15; for i be set st i in the carrier of S holds f.i is Function of (the Sorts of QuotOSAlg (U1, R)).i, (the Sorts of U2).i proof let i be set; assume i in the carrier of S; then reconsider s = i as Element of S; f.s = OSHomQuot(F,R,s) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the Sorts of QuotOSAlg (U1,R),the Sorts of U2 by MSUALG_1:def 2; reconsider f as ManySortedFunction of QuotOSAlg (U1,R),U2; take f; thus thesis by A1; end; uniqueness proof let H,G be ManySortedFunction of QuotOSAlg (U1,R),U2; assume that A2: for s be Element of S holds H.s = OSHomQuot(F,R,s) and A3: for s be Element of S holds G.s = OSHomQuot(F,R,s); now let i be set; assume i in the carrier of S; then reconsider s = i as SortSymbol of S; H.s = OSHomQuot(F,R,s) & G.s = OSHomQuot(F,R,s) by A2,A3; hence H.i = G. i; end; hence thesis by PBOOLE:3; end; end; theorem for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2, R be OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds OSHomQuot(F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot(F,R) is order-sorted proof let U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,U2, R be OSCongruence of U1; set mc = R, qa = QuotOSAlg (U1,mc), qh = OSHomQuot(F,R), S1 = the Sorts of U1; assume A1: F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F; A2: qa = MSAlgebra (# OSClass mc, OSQuotCharact mc #) by Def22; for o be Element of the OperSymbols of S st Args (o,qa) <> {} for x be Element of Args(o,qa) holds (qh.(the_result_sort_of o)).(Den(o,qa).x) = Den(o,U2).(qh#x) proof let o be Element of the OperSymbols of S such that Args (o,qa) <> {}; let x be Element of Args(o,qa); reconsider o1 = o as OperSymbol of S; set ro = the_result_sort_of o, ar = the_arity_of o; A3: Den(o,qa) = (OSQuotCharact mc).o by A2,MSUALG_1:def 11 .= OSQuotCharact(mc,o1) by Def21; Args(o,qa) = ((OSClass mc)# * (the Arity of S)).o by A2,MSUALG_1:def 9; then consider a be Element of Args(o,U1) such that A4: x = mc #_os a by Th15; A5: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1) by FUNCT_2:def 1; o in the OperSymbols of S; then o in dom (S1 * the ResultSort of S) by PBOOLE:def 3; then A6: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the ResultSort of S).o) by FUNCT_1:22 .= (the Sorts of U1).ro by MSUALG_1:def 7; then A7: Result(o,U1) = S1.ro by MSUALG_1:def 10; reconsider da = (Den(o,U1)).a as Element of S1.ro by A6,MSUALG_1:def 10; A8: qh.ro = OSHomQuot(F,R,ro) by Def30; rng Den(o,U1) c= dom OSQuotRes(mc,o) by A5,A6,A7,FUNCT_2:def 1; then A9: dom ((OSQuotRes(mc,o)) * Den(o,U1)) = dom Den(o,U1) by RELAT_1:46; A10: dom (qh # x) = dom ar & dom (F # a) = dom ar & dom x = dom ar & dom a = dom ar by MSUALG_3:6; A11: now let y be set; assume A12: y in dom ar; then reconsider n = y as Nat; A13: ar/.n = ar.n by A12,FINSEQ_4:def 4; ar.n in rng ar by A12,FUNCT_1:def 5; then reconsider s = ar.n as SortSymbol of S; consider an being Element of S1.s such that A14: an = a.n & x.n = OSClass(mc,an) by A4,A12,A13,Def15; (qh # x).n = (qh.s).(x.n) by A10,A12,A13,MSUALG_3:def 8 .= OSHomQuot(F,R,s).OSClass(mc,an) by A14,Def30 .= (F.s).an by A1,Def29 .= (F # a).n by A10,A12,A13,A14,MSUALG_3:def 8; hence (qh # x).y = (F # a).y; end; ar = (the Arity of S).o by MSUALG_1:def 6; then product((OSClass mc) * ar) = ((OSClass mc)# * the Arity of S).o by MSAFREE:1; then Den(o,qa).x = (OSQuotRes(mc,o) * Den(o,U1)).a by A3,A4,Def20 .= (OSQuotRes(mc,o)) . da by A5,A9,FUNCT_1:22 .= OSClass (R,da) by Def16; then (qh.ro).(Den(o,qa).x) = (F.ro).((Den(o,U1)).a) by A1,A8,Def29 .= Den(o,U2).(F#a) by A1,MSUALG_3:def 9; hence thesis by A10,A11,FUNCT_1:9; end; hence qh is_homomorphism qa,U2 by MSUALG_3:def 9; thus OSHomQuot(F,R) is order-sorted proof let s1,s2 being Element of S such that A15: s1 <= s2; let a1 be set such that A16: a1 in dom (qh.s1); reconsider sqa = the Sorts of qa as OrderSortedSet of S by OSALG_1:17; reconsider S1O = S1 as OrderSortedSet of S by OSALG_1:17; A17: S1O.s1 c= S1O.s2 by A15,OSALG_1:def 18; A18: dom (qh.s1) = (the Sorts of qa).s1 & dom (qh.s2) = (the Sorts of qa).s2 by FUNCT_2:def 1; sqa.s1 c= sqa.s2 by A15,OSALG_1:def 18; hence a1 in dom (qh.s2) by A16,A18; qa = MSAlgebra(# OSClass mc, OSQuotCharact mc #) by Def22; then a1 in (OSClass R).s1 by A16; then a1 in OSClass (R,s1) by Def13; then consider x being set such that A19: x in S1.s1 and A20: a1 = Class( CompClass(R,CComp(s1)), x) by Def12; reconsider x1 = x as Element of S1.s1 by A19; reconsider x2 = x as Element of S1.s2 by A17,A19; reconsider s3 = s1, s4 = s2 as Element of S; x1 in dom (F.s3) by A19,FUNCT_2:def 1; then A21: x1 in dom (F.s4) & (F.s3).x1 = (F.s4).x1 by A1,A15,OSALG_3:def 1; A22: a1 = OSClass(R,x1) by A20,Def14; then A23: a1 = OSClass(R,x2) by A15,Th14; thus (qh.s1).a1 = OSHomQuot(F,R,s1).(OSClass(R,x1)) by A22,Def30 .= (F.s2).x1 by A1,A21,Def29 .= OSHomQuot(F,R,s2).(OSClass(R,x2)) by A1,Def29 .= (qh.s2).a1 by A23,Def30; end; end;

Back to top