:: Order Sorted Quotient Algebra :: by Josef Urban :: :: Received September 19, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, ORDERS_2, MSUALG_4, OSALG_1, RELAT_1, STRUCT_0, FUNCOP_1, PBOOLE, SUBSET_1, XXREAL_0, FUNCT_1, MSUALG_1, TARSKI, EQREL_1, NAT_1, MARGREL1, PARTFUN1, FINSEQ_1, ARYTM_3, ARYTM_1, ZFMISC_1, FINSEQ_5, CARD_1, RELAT_2, ORDINAL4, NATTRA_1, YELLOW15, SETFAM_1, COH_SP, YELLOW18, WAYBEL_0, CARD_3, MSUALG_3, WELLORD1, SEQM_3, OSALG_4; notations ZFMISC_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, EQREL_1, SETFAM_1, XCMPLX_0, ORDERS_2, ORDERS_3, NUMBERS, ORDINAL1, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_2, FINSEQ_4, FINSEQ_5, FUNCOP_1, PBOOLE, STRUCT_0, WAYBEL_0, MSUALG_1, MSUALG_3, OSALG_1, OSALG_3, MSUALG_4, XXREAL_0; constructors REAL_1, NAT_1, NAT_D, EQREL_1, FINSEQ_4, FINSEQ_5, MSUALG_3, MSUALG_4, ORDERS_3, WAYBEL_0, OSALG_3, RELSET_1; registrations SUBSET_1, RELAT_1, PARTFUN1, FUNCOP_1, XREAL_0, INT_1, FINSEQ_1, EQREL_1, FUNCT_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, MSUALG_4, ORDERS_3, OSALG_1, ORDINAL1, CARD_3, TOLER_1, RELSET_1, FINSEQ_2; 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, MSUALG_5, OSALG_1, OSALG_3, RELAT_2, ZFMISC_1, RELAT_1, RELSET_1, EQREL_1, MSUALG_3, MSUALG_6, MSAFREE, TARSKI, SYSREL, ORDERS_2, FINSEQ_1, FINSEQ_3, ENUMSET1, FINSEQ_5, INT_1, ORDERS_3, PARTFUN1, WAYBEL_0, GRFUNC_1, MSUALG_9, MSUALG_4, FINSEQ_2, ORDERS_1, FUNCOP_1, XREAL_1, XXREAL_0, XTUPLE_0; schemes FUNCT_1, CLASSES1, NAT_1, FUNCT_2; begin registration let R be non empty Poset; cluster Relation-yielding for OrderSortedSet of R; existence proof set R1 = the Relation; set I = the carrier of R; set f = I --> R1; reconsider f as ManySortedSet of I; f is order-sorted proof let s1,s2 be Element of R such that s1 <= s2; f.s1 = R1 by FUNCOP_1:7; hence thesis by FUNCOP_1:7; 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 FUNCOP_1:7; hence thesis by FUNCOP_1:def 11; 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; registration let R be non empty Poset; let A,B be ManySortedSet of the carrier of R; cluster os-compatible for ManySortedRelation of A,B; existence proof set I = the carrier of R; consider R1 be Relation such that A1: R1 = {}; set f = I --> R1; reconsider f as ManySortedSet of R; set f1 = f; 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,FUNCOP_1:7; hence thesis by RELSET_1:12; end; then reconsider f2 = f1 as ManySortedRelation of A,B by MSUALG_4:def 1; take f; 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; let x,y be set such that x in A.s1 and y in B.s1; f1.s1 = R1 by FUNCOP_1:7 .= f1.s2 by FUNCOP_1:7; hence thesis; end; then f2 is os-compatible by 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; end; theorem Th1: 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; set OR1 = OR; assume A1: OR is os-compatible; 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:87; hence thesis by A1,A2,A3,Def1; end; hence thesis by RELAT_1:def 3; end; hence thesis; end; registration let R be non empty Poset; let A,B be ManySortedSet of R; cluster os-compatible -> order-sorted for ManySortedRelation of A,B; coherence by Th1; 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 :Def2: it is os-compatible; existence proof reconsider Y = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; set X = the 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 registration let S be OrderSortedSign, U1 be OSAlgebra of S; cluster MSEquivalence-like for 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 FUNCT_1:sch 4; reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2,RELAT_1:def 18; 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 1; reconsider f as ManySortedRelation of U1; set f1 = f; A2: f1 is os-compatible proof reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; let s1,s2 be Element of S such that A3: s1 <= s2; reconsider s3 = s1, s4 = s2 as Element of S; let x,y be set such that A4: x in (the Sorts of U1).s1 and y in (the Sorts of U1).s1; A5: f1.s1 = id(X.s1) by A1; A6: f1.s2 = id(X.s2) by A1; X.s3 c= X.s4 by A3,OSALG_1:def 16; then id(X.s1) c= id(X.s2) by SYSREL:15; hence [x,y] in f1.s1 implies [x,y] in f1.s2 by A5,A6; assume [x,y] in f1.s2; then x = y by A6,RELAT_1:def 10; hence thesis by A5,A4,RELAT_1:def 10; end; take f; 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 2; hence thesis by A2,Def2,MSUALG_4:def 3; end; end; :: REVISE: we need the fact that id has the type, :: the original prf can be simplified registration let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster MSCongruence-like for 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 FUNCT_1:sch 4; reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2 ,RELAT_1:def 18; 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 1; 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 2; then reconsider f as MSEquivalence-like ManySortedRelation of U1 by MSUALG_4:def 3; set f1 = f; f1 is os-compatible proof reconsider X = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; let s1,s2 be Element of S such that A2: s1 <= s2; reconsider s3 = s1, s4 = s2 as Element of S; let x,y be set such that A3: x in (the Sorts of U1).s1 and y in (the Sorts of U1).s1; A4: f1.s1 = id(X.s1) by A1; A5: f1.s2 = id(X.s2) by A1; X.s3 c= X.s4 by A2,OSALG_1:def 16; then id(X.s1) c= id(X.s2) by SYSREL:15; hence [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 A4,A3,RELAT_1:def 10; end; then reconsider f = f1 as MSEquivalence-like OrderSortedRelation of U1 by Def2; take f; for o be Element of the carrier' 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 carrier' of S; let x,y be Element of Args(o,U1); A6: dom x = dom (the_arity_of o) by MSUALG_3:6; assume A7: for n be Nat st n in dom x holds [x.n,y.n] in f.((the_arity_of o)/.n); A8: for a be set st a in dom (the_arity_of o) holds x.a = y.a proof set ao = the_arity_of o; let a be set; assume A9: a in dom (the_arity_of o); then reconsider n = a as Nat; ao.n in rng ao by A9,FUNCT_1:def 3; then A10: f.(ao.n) = id ((the Sorts of U1).(ao.n)) by A1; (the_arity_of o)/.n = (the_arity_of o).n by A9,PARTFUN1:def 6; then [x.n,y.n] in f.(ao.n) by A7,A6,A9; hence thesis by A10,RELAT_1:def 10; end; set r = the_result_sort_of o; A11: f.r = id ((the Sorts of U1).r) by A1; A12: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1; then A13: dom ((the Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort of S) by PARTFUN1:def 2; A14: Result(o,U1) = ((the Sorts of U1) * the ResultSort of S).o by MSUALG_1:def 5 .= (the Sorts of U1).((the ResultSort of S).o) by A12,A13,FUNCT_1:12 .= (the Sorts of U1).r by MSUALG_1:def 2; dom y = dom (the_arity_of o) by MSUALG_3:6; then Den(o,U1).x = Den(o,U1).y by A6,A8,FUNCT_1:2; hence thesis by A11,A14,RELAT_1:def 10; end; hence thesis by MSUALG_4:def 4; 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 :Def3: 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 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]}; P c= [:the carrier of R, the carrier of R:] proof let z be set; assume z in P; then ex x,y being Element of R st z = [x,y] & x in the carrier of R & y in the carrier of R & PC[x,y]; hence thesis by ZFMISC_1:87; end; then reconsider P1 = P as Relation of the carrier of R; A1: 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 A2: [x,y] = [x1,y1] and x1 in the carrier of R and y1 in the carrier of R and A3: PC[x1,y1]; x = x1 & y = y1 by A2,XTUPLE_0:1; hence x in the carrier of R & y in the carrier of R & PC[x,y] by A3; end; thus thesis; end; now let x,y be set; assume that A4: x in the carrier of R & y in the carrier of R and A5: [x,y] in P1; consider p being FinSequence of the carrier of R such that A6: 1 < len p and A7: p.1 = x & p.(len p) = y and A8: 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 A1,A5; PC[y,x] proof take F = Rev p; thus 1 < len F by A6,FINSEQ_5:def 3; A9: len F = len p by FINSEQ_5:def 3; hence F.1 = y & F.(len F) = x by A7,FINSEQ_5:62; let n1 be Nat such that A10: 2 <= n1 and A11: n1 <= len F; 1 <= n1 by A10,XXREAL_0:2; then A12: n1 in dom p by A9,A11,FINSEQ_3:25; set n2 = (len p - n1) + 2; 0 <= len p - n1 by A9,A11,XREAL_1:48; then A13: 2 + 0 <= n2 by XREAL_1:6; A14: 2 - 1 <= n1 - 1 by A10,XREAL_1:9; then reconsider n11 = n1 - 1 as Element of NAT by INT_1:3,XXREAL_0:2; n1 - 1 <= len F - 0 by A11,XREAL_1:13; then n11 in dom p by A9,A14,FINSEQ_3:25; then A15: F.(n1 - 1) = p.(len p - (n1 - 1) + 1) by FINSEQ_5:58 .= p.((len p - n1) + 2); reconsider n2 = (len p - n1) + 2 as Element of NAT by A13,INT_1:3 ,XXREAL_0:2; len p - n1 <= len p - 2 by A10,XREAL_1:13; then A16: (len p - n1) + 2 <= len p - 2 + 2 by XREAL_1:6; p.(n2-1) = p.((len p - n1) + (2 - 1)) .= F.n1 by A12,FINSEQ_5:58; hence thesis by A8,A15,A13,A16; end; hence [y,x] in P1 by A4; end; then A17: P1 is_symmetric_in the carrier of R by RELAT_2:def 3; A18: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 2; now let x be set; assume A19: x in the carrier of R; PC[x,x] proof set F = <*x,x*>; rng F = {x,x} by FINSEQ_2:127 .= {x} by ENUMSET1:29; then rng F c= the carrier of R by A19,ZFMISC_1:31; then reconsider F1 = F as FinSequence of the carrier of R by FINSEQ_1:def 4; take F1; A20: len F = 2 by FINSEQ_1:44; hence 1 < len F1; thus F1.1 = x & F1.(len F1) = x by A20,FINSEQ_1:44; let n1 be Nat; assume 2 <= n1 & n1 <= len F1; then A21: n1 = 2 by A20,XXREAL_0:1; F.1 = x & F.2 = x by FINSEQ_1:44; hence thesis by A18,A19,A21,RELAT_2:def 1; end; hence [x,x] in P1 by A19; end; then P1 is_reflexive_in the carrier of R by RELAT_2:def 1; then A22: dom P1 = the carrier of R & field P1 = the carrier of R by ORDERS_1:13; now let x,y,z be set; assume that A23: x in the carrier of R and A24: y in the carrier of R and A25: z in the carrier of R and A26: [x,y] in P1 & [y,z] in P1; ( PC[x,y])& PC[y,z] by A1,A26; then consider p1,p2 being FinSequence of the carrier of R such that A27: 1 < len p1 and A28: p1.1 = x and A29: p1.(len p1) = y and A30: 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 A31: 1 < len p2 and A32: p2.1 = y and A33: p2.(len p2) = z and A34: 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; A35: len F = len p1 + len p2 by FINSEQ_1:22; 1 + 1 < len p1 + len p2 by A27,A31,XREAL_1:8; hence 1 < len F by A35,XXREAL_0:2; 1 in dom p1 by A27,FINSEQ_3:25; hence F.1 = x by A28,FINSEQ_1:def 7; len p2 in dom p2 by A31,FINSEQ_3:25; hence F.(len F) = z by A33,A35,FINSEQ_1:def 7; let n1 be Nat such that A36: 2 <= n1 and A37: n1 <= len F; A38: 1 <= n1 by A36,XXREAL_0:2; A39: 2 - 1 <= n1 - 1 by A36,XREAL_1:9; then reconsider n11 = n1 - 1 as Element of NAT by INT_1:3,XXREAL_0:2; A40: len p1 + 1 <= n1 implies len p1 + 1 = n1 or len p1 + 1 < n1 by XXREAL_0:1; A41: n1 - 1 <= len F - 0 by A37,XREAL_1:13; per cases by A40,INT_1:7; suppose A42: n1 <= len p1; then n1 - 1 <= len p1 - 0 by XREAL_1:13; then n11 in dom p1 by A39,FINSEQ_3:25; then A43: F.(n1 -1) = p1.(n1 - 1) by FINSEQ_1:def 7; n1 in dom p1 by A38,A42,FINSEQ_3:25; then F.n1 = p1.n1 by FINSEQ_1:def 7; hence thesis by A30,A36,A42,A43; end; suppose A44: len p1 + 1 < n1; len p1 < len p1 + 1 by XREAL_1:29; then A45: len p1 < n1 by A44,XXREAL_0:2; then reconsider k = n1 - len p1 as Element of NAT by INT_1:3 ,XREAL_1:48; (len p1 + 1) - 1 < n1 - 1 by A44,XREAL_1:9; then F.n11 = p2.(n11 - len p1) by A41,FINSEQ_1:24; then A46: F.(n1 - 1) = p2.(k - 1); 1 < n1 - len p1 by A44,XREAL_1:20; then A47: 1 + 1 <= n1 - len p1 by INT_1:7; n1 <= len p1 + len p2 by A37,FINSEQ_1:22; then A48: k <= len p2 by XREAL_1:20; F.n1 = p2.k by A37,A45,FINSEQ_1:24; hence thesis by A34,A46,A47,A48; end; suppose A49: len p1 + 1 = n1; len p1 + 1 <= len p1 + len p2 & (len p1 + 1) - len p1 = 1 by A31, XREAL_1:8; then A50: F.n1 = y by A32,A49,FINSEQ_1:23; len p1 in dom p1 by A27,FINSEQ_3:25; then F.(n1 - 1) = y by A29,A49,FINSEQ_1:def 7; hence thesis by A18,A24,A50,RELAT_2:def 1; end; end; hence [x,z] in P1 by A23,A25; 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 A22,A17, PARTFUN1:def 2,RELAT_2:def 11,def 16; take P1; thus thesis by A1; end; uniqueness proof let X,Y be Equivalence_Relation of the carrier of R; 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; assume A51: for x,y being set holds [x,y] in X iff PC1[x,y]; assume A52: 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 A51; hence [x,y] in Y by A52; end; assume [x,y] in Y; then PC1[x,y] by A52; hence thesis by A51; 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:44; A3: p.1 = s1 by FINSEQ_1:44; A4: 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; assume 2 <= n1 & n1 <= len p; then A5: n1 = 2 by A2,XXREAL_0:1; [s1,s2] in the InternalRel of R by A1,ORDERS_2:def 5; hence thesis by A3,A5,FINSEQ_1:44; end; p.(len p) = s2 by A2,FINSEQ_1:44; hence thesis by A2,A3,A4,Def3; 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 :Def4: [s1,s2] in Path_Rel R; reflexivity proof set PR = Path_Rel R; field PR = the carrier of R by ORDERS_1:12; 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:12; 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; set PR = Path_Rel R; field PR = the carrier of R by ORDERS_1:12; then A1: PR is_transitive_in the carrier of R by RELAT_2:def 16; assume s1 ~= s2 & s2 ~= s3; then [s1,s2] in PR & [s2,s3] in PR by Def4; then [s1,s3] in PR by A1,RELAT_2:def 8; hence thesis by Def4; end; :: do for Relations definition let R be non empty Poset; func Components R -> non empty (Subset-Family of R) equals Class Path_Rel R; coherence; end; registration let R be non empty Poset; cluster -> non empty for Element of Components R; coherence proof let X be Element of Components R; ex x being set st x in the carrier of R & X = Class( Path_Rel R,x) by EQREL_1:def 3; hence thesis by EQREL_1:20; end; end; definition let R be non empty Poset; mode Component of R is Element of Components R; end; definition let R be non empty Poset; let s1 be Element of R; func CComp s1 -> Component of R equals Class(Path_Rel R,s1); correctness by EQREL_1:def 3; end; theorem Th4: 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; assume s1 <= s2; then [s1,s2] in Path_Rel R by Th2; hence thesis by EQREL_1:35; 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 union {A.s where s is Element of R: s in C}; correctness; end; theorem Th5: 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 EQREL_1:20; then A.s in {A.s1 where s1 is Element of R: s1 in CComp(s)}; hence thesis by A1,TARSKI:def 4; end; definition let R be non empty Poset; attr R is locally_directed means :Def8: for C being Component of R holds C is directed; end; theorem Th6: 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 and A2: p.1 = x and A3: p.(len p) = y and A4: 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 Def3; for n1 being Nat st 1 <= n1 & n1 <= len p holds p.n1 = x proof defpred P[Nat] means p.$1 <> x & 1 <= $1; let n1 be Nat such that A5: 1 <= n1 and A6: n1 <= len p; assume A7: p.n1 <> x; then A8: ex k being Nat st P[k] by A5; consider k being Nat such that A9: P[k] & for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A8); 1 < k by A2,A9,XXREAL_0:1; then A10: 1 + 1 <= k by INT_1:7; then A11: 1 + 1 - 1 <= k - 1 by XREAL_1:9; then reconsider k1 = k - 1 as Element of NAT by INT_1:3,XXREAL_0:2; A12: p.k1 = x by A9,A11,XREAL_1:146; k <= n1 by A5,A7,A9; then A13: k <= len p by A6,XXREAL_0:2; then k in dom p by A9,FINSEQ_3:25; then reconsider pk = p.k as Element of R by PARTFUN1:4; per cases by A4,A10,A13,A12; suppose [pk,x] in the InternalRel of R; then pk <= x by ORDERS_2:def 5; hence contradiction by A9,ORDERS_3:1; end; suppose [x,pk] in the InternalRel of R; then x <= pk by ORDERS_2:def 5; hence contradiction by A9,ORDERS_3:1; end; end; hence thesis by A1,A3; end; theorem Th7: 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; 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 3; 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 reconsider y1 = y as Element of R; [y,x] in Path_Rel R by A2,A3,EQREL_1:19; then y1 = x1 by Th6; hence y = x1; end; assume y = x1; hence thesis by A2,EQREL_1:20; end; hence thesis by TARSKI:def 1; end; theorem Th8: 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 Th7; 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 and A3: y1 in C; take x1; x1 = x by A1,A2,TARSKI:def 1; hence thesis by A1,A3,TARSKI:def 1; end; hence thesis by WAYBEL_0:def 1; end; :: the system could generate this one from the following registration cluster locally_directed for non empty Poset; existence proof set R = the discrete non empty Poset; take R; thus thesis by Th8; end; end; registration cluster locally_directed for OrderSortedSign; existence proof set R = the discrete OrderSortedSign; take R; thus thesis by Th8; end; end; registration cluster discrete -> locally_directed for non empty Poset; coherence by Th8; end; registration let S be locally_directed non empty Poset; cluster -> directed for Component of S; coherence by Def8; end; theorem Th9: {} is Equivalence_Relation of {} by RELSET_1:12; :: 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 :Def9: 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 Def2; 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; x in (the Sorts of A).s1 & (the Sorts of A).s1 in {(the Sorts of A ).s where s is Element of S: s in C} by A3,ZFMISC_1:87; hence thesis by A2,TARSKI:def 4; end; hence thesis by A2,Th9; end; 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]}; CC c= [:SAC, SAC:] proof let z be set; assume z in CC; then ex x,y being Element of SAC st z = [x,y] & CC1[x,y]; hence thesis by ZFMISC_1:87; end; then reconsider P1 = CC as Relation of SAC; now let x,y be set such that A4: x in SAC & y in SAC and A5: [x,y] in P1; reconsider x1 = x, y1 = y as Element of SAC by A4; consider x2,y2 being Element of SAC such that A6: [x,y] = [x2,y2] and A7: CC1[x2,y2] by A5; A8: x = x2 & y = y2 by A6,XTUPLE_0:1; consider s5 being Element of S such that A9: s5 in C and A10: [x2,y2] in E.s5 by A7; field(E.s5) = (the Sorts of A).s5 by ORDERS_1:12; then A11: E.s5 is_symmetric_in (the Sorts of A).s5 by RELAT_2:def 11; x2 in (the Sorts of A).s5 & y2 in (the Sorts of A).s5 by A10, ZFMISC_1:87; then [y,x] in E.s5 by A8,A10,A11,RELAT_2:def 3; then [y1,x1] in CC by A9; hence [y,x] in P1; end; then A12: P1 is_symmetric_in SAC by RELAT_2:def 3; now let x be set such that A13: x in SAC; reconsider x1 = x as Element of SAC by A13; 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 A13, TARSKI:def 4; consider s being Element of S such that A16: X = (the Sorts of A).s and A17: s in C by A15; field(E.s) = (the Sorts of A).s by ORDERS_1:12; 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 A17; hence [x,x] in P1; end; then P1 is_reflexive_in SAC by RELAT_2:def 1; then A18: dom P1 = SAC & field P1 = SAC by ORDERS_1:13; now let x,y,z be set such that x in SAC and y in SAC and z in SAC and A19: [x,y] in P1 and A20: [y,z] in P1; consider x2,y2 being Element of SAC such that A21: [x,y] = [x2,y2] and A22: CC1[x2,y2] by A19; A23: x = x2 by A21,XTUPLE_0:1; consider y3,z3 being Element of SAC such that A24: [y,z] = [y3,z3] and A25: CC1[y3,z3] by A20; A26: y = y3 by A24,XTUPLE_0:1; consider s5 being Element of S such that A27: s5 in C and A28: [x2,y2] in E.s5 by A22; consider s6 being Element of S such that A29: s6 in C and A30: [y3,z3] in E.s6 by A25; reconsider s51 = s5, s61 = s6 as Element of S; consider su being Element of S such that A31: su in C and A32: s51 <= su and A33: s61 <= su by A27,A29,WAYBEL_0:def 1; y3 in (the Sorts of A).s6 & z3 in (the Sorts of A).s6 by A30, ZFMISC_1:87; then A34: [y3,z3] in E.su by A1,A30,A33,Def1; then A35: z3 in (the Sorts of A).su by ZFMISC_1:87; A36: z = z3 by A24,XTUPLE_0:1; A37: y = y2 by A21,XTUPLE_0:1; field(E.su) = (the Sorts of A).su by ORDERS_1:12; then A38: E.su is_transitive_in (the Sorts of A).su by RELAT_2:def 16; x2 in (the Sorts of A).s5 & y2 in (the Sorts of A).s5 by A28, ZFMISC_1:87; then A39: [x2,y2] in E.su by A1,A28,A32,Def1; then x2 in (the Sorts of A).su & y2 in (the Sorts of A).su by ZFMISC_1:87; then [x2,z3] in E.su by A37,A26,A39,A34,A35,A38,RELAT_2:def 8; hence [x,z] in P1 by A23,A36,A31; 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 A18,A12,PARTFUN1:def 2,RELAT_2:def 11,def 16; take P1; 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 ex x1,y1 being Element of SAC st [x,y] = [x1,y1] & CC1[x1,y1]; hence CC1[x,y]; end; assume A40: CC1[x,y]; then consider s1 being Element of S such that A41: s1 in C and A42: [x,y] in E.s1; A43: y in (the Sorts of A).s1 by A42,ZFMISC_1:87; (the Sorts of A).s1 in {(the Sorts of A).s where s is Element of S: s in C} & x in (the Sorts of A).s1 by A41,A42,ZFMISC_1:87; then reconsider x1 = x, y1 =y as Element of SAC by A43,TARSKI:def 4; [x1,y1] in CC by A40; hence thesis; end; hence thesis; end; end; uniqueness proof let X,Y be Equivalence_Relation of (the Sorts of A)-carrier_of C; defpred CC1[set,set] means ex s1 being Element of S st s1 in C & [$1,$2] in E.s1; assume A44: for x,y being set holds [x,y] in X iff CC1[x,y]; assume A45: 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 A44; hence [x,y] in Y by A45; end; assume [x,y] in Y; then CC1[x,y] by A45; hence thesis by A44; 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 :Def10: 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 set SAC = (the Sorts of A)-carrier_of CComp(s1); set CS = Class(CompClass(E,CComp(s1))); defpred CC1[set] means ex x being set st x in (the Sorts of A).s1 & $1 = Class( CompClass(E,CComp(s1)), x); 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 and z = Class( CompClass(E,CComp(s1)), x); x in SAC by A2,Th5; hence thesis by A1; end; 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 ex y being Element of CS1 st x = y & CC1[y]; hence x in CS1; 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 ex x1 being Element of CS1 st x = x1 & CC1[x1]; hence CC1[x]; end; assume A3: CC1[x]; then consider y being set such that A4: y in (the Sorts of A).s1 and A5: x = Class( CompClass(E,CComp(s1)), y); s1 in CComp(s1) by EQREL_1:20; then (the Sorts of A).s1 in {(the Sorts of A).s where s is Element of S: s in CComp(s1)}; then y in union {(the Sorts of A).s where s is Element of S: s in CComp(s1)} by A4,TARSKI:def 4; then x in Class( CompClass(E,CComp(s1))) by A5,EQREL_1:def 3; hence thesis by A3; end; hence thesis; end; end; uniqueness proof let X,Y be Subset of Class(CompClass(E,CComp(s1))); defpred CC1[set] means ex x being set st x in (the Sorts of A).s1 & $1 = Class( CompClass(E,CComp(s1)), x); assume A6: for x being set holds x in X iff CC1[x]; assume A7: 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 A6; hence x in Y by A7; end; assume x in Y; then CC1[x] by A7; hence thesis by A6; end; hence thesis by TARSKI:1; end; end; registration 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,Def10; hence thesis; end; end; theorem Th10: 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 Th4; thus OSClass(E,s1) c= OSClass(E,s2) proof reconsider SO = the Sorts of A as OrderSortedSet of S by OSALG_1:17; let z be set; assume z in OSClass(E,s1); then A3: ex x being set st x in (the Sorts of A).s1 & z = Class( CompClass(E, CComp(s1)), x) by Def10; SO.s3 c= SO.s4 by A1,OSALG_1:def 16; hence thesis by A2,A3,Def10; 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 :Def11: 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 FUNCT_1:sch 4; reconsider f1 = f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2 ,RELAT_1:def 18; 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 thesis by A3,Th10; 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; registration 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; assume i in the carrier of S; then reconsider s = i as Element of S; (OSClass E).s = OSClass( E,s) by Def11; hence thesis; end; hence thesis by PBOOLE:def 13; 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 Class( CompClass(E, CComp(s)), x); correctness by Def10; 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; assume ex z being Element of R st z <= x & z <= y; then consider z being Element of R such that A1: z <= x and A2: z <= y; reconsider x1 = x,y1 = y as Element of R; CComp(z) = CComp(y) by A2,Th4; then A3: y in CComp(z) by EQREL_1:20; CComp z = CComp(x) by A1,Th4; then x in CComp(z) by EQREL_1:20; then ex u being Element of R st u in CComp(z) & x1 <= u & y1 <= u by A3, WAYBEL_0:def 1; hence thesis; end; theorem Th12: 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: s in CComp(s) by EQREL_1:20; A2: E is os-compatible by Def2; A3: x in (the Sorts of U1)-carrier_of CComp(s) by Th5; hereby assume OSClass(E,x) = OSClass(E,y); then [x,y] in CompClass(E, CComp(s)) by A3,EQREL_1:35; then consider s1 being Element of S such that A4: s1 in CComp(s) and A5: [x,y] in E.s1 by Def9; reconsider sn1 = s, s11 = s1 as Element of S; consider s2 being Element of S such that s2 in CComp(s) and A6: s11 <= s2 and A7: sn1 <= s2 by A1,A4,WAYBEL_0:def 1; x in SU.s11 & y in SU.s11 by A5,ZFMISC_1:87; then [x,y] in E.s2 by A2,A5,A6,Def1; hence [x,y] in E.s by A2,A7,Def1; end; A8: s in CComp(s) by EQREL_1:20; A9: x in (the Sorts of U1)-carrier_of CComp(s) by Th5; assume [x,y] in E.s; then [x,y] in CompClass(E, CComp(s)) by A8,Def9; hence thesis by A9,EQREL_1:35; end; theorem 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) by Th4; begin :: Order Sorted Quotient Algebra :: take care (or even prove counterexample) - order-sorted :: ManySortedFunction generaly does not exist reserve S for locally_directed OrderSortedSign; reserve o for Element of the carrier' 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 : Def13: 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 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); set ar = the_arity_of o, da = dom ar; 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 CLASSES1: sch 1(A1); A4: dom ((OSClass R) * ar) = da by PARTFUN1:def 2; 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 reconsider n = y as Nat; ar.y in rng ar by A4,A5,FUNCT_1:def 3; then reconsider s = ar.y as Element of S; (ex z being Element of (the Sorts of A).((the_arity_of o)/.n ) st z = x.n & f.n = OSClass(R, z) )& ((ar)/.n) = ar.n by A3,A4,A5,PARTFUN1:def 6; then A6: f.y in OSClass (R,s); ((OSClass R) * ar).y = (OSClass R).(ar.y) by A5,FUNCT_1:12; hence thesis by A6,Def11; end; then reconsider f as Element of product ((OSClass R) * ar) by A3,A4, CARD_3:9; 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 A7: ( 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))& 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); A8: for y be set st y in dom (the_arity_of o) holds F.y = G.y proof let y be set; assume A9: y in dom (the_arity_of o); then reconsider n = y as Nat; (ex z being Element of (the Sorts of A).((the_arity_of o)/.n ) st z = x.n & F.n = OSClass(R, z) )& ex z1 being Element of (the Sorts of A).(( the_arity_of o )/. n) st z1 = x.n & G.n = OSClass(R, z1) by A7,A9; hence thesis; end; A10: dom G = dom (the_arity_of o) by PARTFUN1:def 2; dom F = dom (the_arity_of o) by PARTFUN1:def 2; hence thesis by A10,A8,FUNCT_1:2; 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 :Def14: 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 FUNCT_1: sch 4; A2: 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 Def11; end; o in the carrier' of S; then o in dom ((the Sorts of A)*(the ResultSort of S)) by PARTFUN1:def 2; then A3: ((the Sorts of A) * the ResultSort of S).o = (the Sorts of A).((the ResultSort of S).o) by FUNCT_1:12 .= D by MSUALG_1:def 2; A4: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1; then dom ((OSClass R) * the ResultSort of S) = dom (the ResultSort of S) by PARTFUN1:def 2; then ((OSClass R) * the ResultSort of S).o = (OSClass R).((the ResultSort of S).o) by A4,FUNCT_1:12 .= (OSClass R).rs by MSUALG_1:def 2; then reconsider f as Function of ((the Sorts of A) * the ResultSort of S).o, (( OSClass R) * the ResultSort of S).o by A1,A3,A2,FUNCT_2:3; take f; thus thesis by A1; end; uniqueness proof set SA = the Sorts of A, RS = the ResultSort of S, rs = the_result_sort_of o; let f,g be Function of ((the Sorts of A) * the ResultSort of S).o, (( OSClass R) * the ResultSort of S).o; assume that A5: for x being Element of SA.rs holds f.x = OSClass(R,x) and A6: for x being Element of SA.rs holds g.x = OSClass(R,x); A7: now let x be set; assume x in SA.rs; then reconsider x1 = x as Element of SA.rs; f.x1 = OSClass(R,x1) by A5; hence f.x = g.x by A6; end; o in the carrier' of S; then o in dom (SA*RS) by PARTFUN1:def 2; then (SA * RS).o = SA.(RS.o) by FUNCT_1:12 .= SA.rs by MSUALG_1:def 2; then dom f = SA.rs & dom g = SA.rs by FUNCT_2:def 1; hence thesis by A7,FUNCT_1:2; 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 ao = the_arity_of o; set D = Args(o,A); deffunc F(Element of D) = R #_os $1; consider f be Function such that A8: dom f = D & for d be Element of D holds f.d = F(d) from FUNCT_1: sch 4; A9: o in the carrier' of S; then o in dom ((the Sorts of A)# * the Arity of S) by PARTFUN1:def 2; then A10: ((the Sorts of A)# * the Arity of S).o = (the Sorts of A)#.((the Arity of S).o) by FUNCT_1:12 .= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 1; A11: 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 A10,MSUALG_1:def 4; f.x1 = R #_os x1 & (OSClass R)#.ao = product((OSClass R)*ao) by A8, FINSEQ_2:def 5; hence thesis; end; o in dom ((OSClass R)# * the Arity of S) by A9,PARTFUN1:def 2; then ((OSClass R)# * the Arity of S).o = (OSClass R)#.((the Arity of S).o) by FUNCT_1:12 .= (OSClass R)#.ao by MSUALG_1:def 1; then reconsider f as Function of ((the Sorts of A)# * the Arity of S).o, (( OSClass R)# * the Arity of S).o by A8,A10,A11,FUNCT_2:3,MSUALG_1:def 4; take f; thus thesis by A8; end; uniqueness proof set ao = the_arity_of o; let f,g be Function of ((the Sorts of A)# * the Arity of S).o, ((OSClass R )# * the Arity of S).o; assume that A12: for x be Element of Args(o,A) holds f.x = R #_os x and A13: for x be Element of Args(o,A) holds g.x = R #_os x; o in the carrier' of S; then o in dom ((the Sorts of A)# * the Arity of S) by PARTFUN1:def 2; then A14: ((the Sorts of A)# * the Arity of S).o = (the Sorts of A)#.((the Arity of S).o) by FUNCT_1:12 .= ((the Sorts of A)#.(the_arity_of o)) by MSUALG_1:def 1; A15: now let x be set; assume x in (the Sorts of A)#.ao; then reconsider x1 = x as Element of Args(o,A) by A14,MSUALG_1:def 4; f.x1 = R #_os x1 by A12; hence f.x = g.x by A13; end; dom f = (the Sorts of A)#.ao & dom g = (the Sorts of A)#.ao by A14, FUNCT_2:def 1; hence thesis by A15,FUNCT_1:2; 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 defpred P[set,set] means for o be OperSymbol of S st o = $1 holds $2 = OSQuotRes(R,o); set O = the carrier' of S; 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 CLASSES1: sch 1( A1); reconsider f as ManySortedSet of O by A2,PARTFUN1:def 2,RELAT_1:def 18; 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; f.x1 = OSQuotRes(R,x1) by A2; hence thesis; end; then reconsider f as ManySortedFunction of O by FUNCOP_1:def 6; 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 PBOOLE:def 15; 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 carrier' of S; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotRes(R,i1) by A3; hence f.i = g.i by A4; 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 defpred P[set,set] means for o be OperSymbol of S st o = $1 holds $2 = OSQuotArgs(R,o); set O = the carrier' of S; 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 CLASSES1: sch 1( A5); reconsider f as ManySortedSet of O by A6,PARTFUN1:def 2,RELAT_1:def 18; 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; f.x1 = OSQuotArgs(R,x1) by A6; hence thesis; end; then reconsider f as ManySortedFunction of O by FUNCOP_1:def 6; 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 PBOOLE:def 15; 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 carrier' of S; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotArgs(R,i1) by A7; hence f.i = g.i by A8; end; hence thesis by PBOOLE:3; end; end; theorem Th14: 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 1; 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 and A4: dom f = dom ((OSClass R) * ar) and A5: 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; defpred P[set,set] means $2 in (the Sorts of A).((ar)/.$1) & $2 in f.$1; A6: dom ((OSClass R) * ar) = dom ar by PARTFUN1:def 2; A7: for n be Nat st n in dom f holds f.n in OSClass (R,((ar)/.n)) proof let n be Nat; reconsider s = ((ar)/.n) as Element of S; assume A8: n in dom f; then ar.n = ((ar)/.n) by A4,A6,PARTFUN1:def 6; then ((OSClass R) * ar).n = (OSClass R).s by A4,A8,FUNCT_1:12 .= OSClass (R,s) by Def11; hence thesis by A4,A5,A8; end; A9: for a be set st a in dom f ex b be set st P[a,b] proof let a be set; reconsider s = ((ar)/.a) as Element of S; assume A10: a in dom f; then reconsider n = a as Nat by A4; f.n in OSClass (R,s) by A7,A10; then consider x being set such that A11: x in (the Sorts of A).s & f.n = Class( CompClass(R,CComp(s)), x) by Def10; take x; thus thesis by A11,Th5,EQREL_1:20; end; consider g be Function such that A12: dom g = dom f & for a be set st a in dom f holds P[a,g.a] from CLASSES1:sch 1(A9); dom (the Sorts of A) = the carrier of S by PARTFUN1:def 2; then rng ar c= dom (the Sorts of A); then A13: dom g = dom ((the Sorts of A) * ar) by A4,A6,A12,RELAT_1:27; A14: 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 A15: y in dom ((the Sorts of A) * ar); then reconsider n = y as Nat; reconsider s = ((ar)/.n) as Element of S; ar.n = ((ar)/.n) & g.n in (the Sorts of A).s by A4,A6,A12,A13,A15, PARTFUN1:def 6; hence thesis by A15,FUNCT_1:12; end; Args(o,A) = ((the Sorts of A)# * (the Arity of S)).o by MSUALG_1:def 4 .= product ((the Sorts of A) * ar) by A2,MSAFREE:1; then reconsider g as Element of Args(o,A) by A13,A14,CARD_3:9; A16: 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; A18: (ex z being Element of (the Sorts of A).((the_arity_of o)/.n ) st z = g.n & (R #_os g).n = OSClass(R, z) )& g.n in f.n by A4,A6,A12,A17,Def13; reconsider s = ((ar)/.n) as Element of S; f.n in OSClass (R,s) by A4,A6,A7,A17; then consider u being set such that A19: u in (the Sorts of A).s and A20: f.n = Class( CompClass(R,CComp(s)), u) by Def10; u in (the Sorts of A)-carrier_of CComp(s) by A19,Th5; hence thesis by A18,A20,EQREL_1:23; end; take g; dom (R #_os g) = dom ((OSClass R) * ar) by CARD_3:9; hence thesis by A3,A4,A6,A16,FUNCT_1:2; 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 :Def18: 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 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; set Ca = ((OSClass R)# * the Arity of S).o, Cr = ((OSClass R) * the ResultSort of S).o; A1: for x be set st x in Ca ex y be set st y in Cr & P[x,y] proof set ro = the_result_sort_of o, ar = the_arity_of o; 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 Th14; take y = ((OSQuotRes(R,o)) * (Den(o,A))).a; A3: o in the carrier' of S; then o in dom ((OSClass R) * the ResultSort of S) by PARTFUN1:def 2; then A4: ((OSClass R) * the ResultSort of S).o = (OSClass R).((the ResultSort of S).o) by FUNCT_1:12 .= (OSClass R).ro by MSUALG_1:def 2; o in dom ((the Sorts of A) * the ResultSort of S) by A3,PARTFUN1:def 2; then A5: ((the Sorts of A) * the ResultSort of S).o = (the Sorts of A).((the ResultSort of S).o) by FUNCT_1:12 .= (the Sorts of A).ro by MSUALG_1:def 2; then A6: dom (OSQuotRes(R,o)) = (the Sorts of A).ro & Result(o,A) = (the Sorts of A). ro by FUNCT_2:def 1,MSUALG_1:def 5; rng Den(o,A) c= Result(o,A); then A7: dom Den(o,A) = Args(o,A) & dom (OSQuotRes(R,o) * Den(o,A)) = dom Den(o,A) by A6,FUNCT_2:def 1,RELAT_1:27; OSQuotRes(R,o).(Den(o,A).a) in rng (OSQuotRes(R,o)) by A6,FUNCT_1:def 3; then OSQuotRes(R,o).(Den(o,A).a) in (OSClass R).ro by A4; hence y in Cr by A4,A7,FUNCT_1:12; let b be Element of Args(o,A); reconsider da = (Den(o,A)).a, db = (Den(o,A)).b as Element of (the Sorts of A).ro by A5,MSUALG_1:def 5; A8: ((OSQuotRes(R,o)) * (Den(o,A))).b = (OSQuotRes(R,o)).db by A7,FUNCT_1:12 .= OSClass(R,db) by Def14 .= Class( CompClass(R, CComp(ro)), db); assume A9: x = R #_os b; for n be Nat st n in dom a holds [a.n,b.n] in R.((ar)/.n) proof let n be Nat; A10: dom a = dom ar by MSUALG_3:6; assume n in dom a; then (ex ya being Element of (the Sorts of A).((ar)/.n) st ya = a.n & (R #_os a). n = OSClass(R, ya) )& ex yb being Element of (the Sorts of A).((ar) /.n) st yb = b.n & (R #_os b).n = OSClass(R, yb) by A10,Def13; hence thesis by A2,A9,Th12; end; then ro in CComp(ro) & [da,db] in R.ro by EQREL_1:20,MSUALG_4:def 4; then A11: [da,db] in CompClass(R, CComp(ro)) by Def9; A12: da in (the Sorts of A)-carrier_of CComp(ro) by Th5; y = (OSQuotRes(R,o)).((Den(o,A)).a) by A7,FUNCT_1:12 .= OSClass(R, da) by Def14 .= Class( CompClass(R, CComp(ro)), da); hence thesis by A12,A8,A11,EQREL_1:35; end; consider f be Function such that A13: dom f = Ca & rng f c= Cr & for x be set st x in Ca holds P[x,f.x] from FUNCT_1:sch 5(A1); reconsider f as Function of ((OSClass R)# * the Arity of S).o, ((OSClass R ) * the ResultSort of S).o by A13,FUNCT_2:2; take f; thus thesis by A13; end; uniqueness proof set ao = the_arity_of o; let F,G be Function of ((OSClass R)# * the Arity of S).o, ((OSClass R) * the ResultSort of S).o; assume that A14: 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 A15: 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; A16: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1; then dom ((OSClass R)# * the Arity of S) = dom (the Arity of S) by PARTFUN1:def 2; then A17: ((OSClass R)# * the Arity of S).o = (OSClass R)#.((the Arity of S).o) by A16,FUNCT_1:12 .= (OSClass R)#.ao by MSUALG_1:def 1; A18: now let x be set; assume A19: x in (OSClass R)#.ao; then consider a be Element of Args(o,A) such that A20: x = R #_os a by A17,Th14; F.x = (OSQuotRes(R,o) * Den(o,A)).a by A14,A17,A19,A20; hence F.x = G.x by A15,A17,A19,A20; end; dom F = (OSClass R)#.ao & dom G = (OSClass R)#.ao by A17,FUNCT_2:def 1; hence thesis by A18,FUNCT_1:2; 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 :Def19: for o be OperSymbol of S holds it.o = OSQuotCharact(R,o); existence proof defpred P[set,set] means for o be OperSymbol of S st o = $1 holds $2 = OSQuotCharact(R,o); set O = the carrier' of S; 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 CLASSES1: sch 1( A1); reconsider f as ManySortedSet of O by A2,PARTFUN1:def 2,RELAT_1:def 18; 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; f.x1 = OSQuotCharact(R,x1) by A2; hence thesis; end; then reconsider f as ManySortedFunction of O by FUNCOP_1:def 6; 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 PBOOLE:def 15; 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 carrier' of S; then reconsider i1 = i as OperSymbol of S; f.i1 = OSQuotCharact(R,i1) by A3; hence f.i = g.i by A4; 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 MSAlgebra(# OSClass R, OSQuotCharact R #); coherence by OSALG_1:17; end; :: we could note that for discrete the QuotOSAlg and QuotMsAlg are equal registration let S; let U1 be non-empty OSAlgebra of S; let R be OSCongruence of U1; cluster QuotOSAlg (U1,R) -> strict non-empty; coherence by MSUALG_1:def 3; 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 :Def21: 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 FUNCT_2:sch 4; 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: 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) by A1; hence f.x = g.x by A2; end; dom f = (the Sorts of U1).s & dom g = (the Sorts of U1).s by FUNCT_2:def 1; hence thesis by A3,FUNCT_1:2; 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 : Def22: 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 FUNCT_1:sch 4; reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2 ,RELAT_1:def 18; 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; f.y = OSNat_Hom(U1,R,y) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6; 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; OSClass(R,s) = (OSClass R).i & f.s = OSNat_Hom(U1,R,s) by A1,Def11; hence thesis; end; then reconsider f as ManySortedFunction of the Sorts of U1,OSClass R by PBOOLE:def 15; 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 A2: for s be Element of S holds F.s = OSNat_Hom(U1,R,s) and A3: 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) by A2; hence F.i = G.i by A3; 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; for o be Element of the carrier' 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 carrier' 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; (the Arity of S).o = ar by MSUALG_1:def 1; then A1: ((OSClass R)# * the Arity of S).o = product ((OSClass R) * ar) by MSAFREE:1 ; A2: dom x = dom ar by MSUALG_3:6; A3: for a be set st a in dom ar holds (F#x).a = (R #_os x).a proof let a be set; assume A4: a in dom ar; then reconsider n = a as Nat; set Fo = OSNat_Hom(U1,R,((ar)/.n)), s = ((ar)/.n); A5: ex z being Element of S1.s st z = x.n & (R #_os x).n = OSClass(R,z) by A4,Def13; A6: n in dom ((the Sorts of U1) * ar) by A4,PARTFUN1:def 2; then ((the Sorts of U1) * ar).n = (the Sorts of U1).(ar.n) by FUNCT_1:12 .= S1.s by A4,PARTFUN1:def 6; then reconsider xn = x.n as Element of S1.s by A6,MSUALG_3:6; thus (F#x).a = (F.((ar)/.n)).(x.n) by A2,A4,MSUALG_3:def 6 .= Fo.xn by Def22 .= (R #_os x).a by A5,Def21; end; dom (the Sorts of U1) = the carrier of S by PARTFUN1:def 2; then rng (the ResultSort of S) c= dom (the Sorts of U1); then dom (the ResultSort of S) = the carrier' of S & dom ((the Sorts of U1 ) * the ResultSort of S) = dom (the ResultSort of S) by FUNCT_2:def 1 ,RELAT_1:27; then A7: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the ResultSort of S).o) by FUNCT_1:12 .= (the Sorts of U1).ro by MSUALG_1:def 2; then reconsider dx = (Den(o,U1)).x as Element of S1.ro by MSUALG_1:def 5; rng Den(o,U1) c= Result(o,U1) & Result(o,U1) = S1.ro by A7,MSUALG_1:def 5; then rng Den(o,U1) c= dom OSQuotRes(R,o) by A7,FUNCT_2:def 1; then A8: dom Den(o,U1) = Args(o,U1) & dom ((OSQuotRes(R,o)) * Den(o,U1)) = dom Den(o, U1) by FUNCT_2:def 1,RELAT_1:27; dom (OSClass R) = the carrier of S by PARTFUN1:def 2; then dom (R #_os x) = dom ((OSClass R) * (the_arity_of o)) & rng ar c= dom ( OSClass R) by CARD_3:9; then dom (F#x) = dom ar & dom (R #_os x) = dom ar by MSUALG_3:6,RELAT_1:27; then A9: F # x = R #_os x by A3,FUNCT_1:2; Den(o,QA) = (OSQuotCharact R).o by MSUALG_1:def 6 .= OSQuotCharact(R,o) by Def19; then Den(o,QA).(F#x) = ((OSQuotRes(R,o)) * (Den(o,U1))).x by A1,A9,Def18 .= (OSQuotRes(R,o)) . dx by A8,FUNCT_1:12 .= OSClass (R, dx) by Def14 .= (OSNat_Hom(U1,R,ro)).dx by Def21 .= (F.ro).((Den(o,U1)).x) by Def22; hence thesis; end; hence F is_homomorphism U1,QA by MSUALG_3:def 7; 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 PBOOLE:def 15; A10: dom f = S1.s by FUNCT_2:def 1; A11: (the Sorts of QA).s = OSClass (R,s) by Def11; for x be set st x in (the Sorts of QA).i holds x in rng f proof let x be set; A12: f = OSNat_Hom(U1,R,s) by Def22; assume x in (the Sorts of QA).i; then consider a1 being set such that A13: a1 in S1.s and A14: x = Class(CompClass(R,CComp(s)),a1) by A11,Def10; reconsider a2 = a1 as Element of S1.s by A13; OSClass(R,a2) = x & f.a1 in rng f by A10,A13,A14,FUNCT_1:def 3; hence thesis by A12,Def21; 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 reconsider S2 = S1 as OrderSortedSet of S by OSALG_1:17; let s1,s2 be Element of S such that A15: s1 <= s2; A16: S2.s1 c= S2.s2 by A15,OSALG_1:def 16; let a1 be set such that A17: a1 in dom (F.s1); A18: a1 in S1.s1 by A17; then reconsider b2 = a1 as Element of S1.s2 by A16; dom (F.s2) = S1.s2 by FUNCT_2:def 1; hence a1 in dom (F.s2) by A16,A18; reconsider b1 = a1 as Element of S1.s1 by A17; thus (F.s1).a1 = OSNat_Hom(U1,R,s1).b1 by Def22 .= OSClass(R,b1) by Def21 .= OSClass(R,b2) by A15,Th4 .= OSNat_Hom(U1,R,s2).b2 by Def21 .= (F.s2).a1 by Def22; end; end; theorem Th16: 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 and A2: 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 A3: s1 <= s2; reconsider s3 = s1, s4 = s2 as SortSymbol of S; let x,y be set such that A4: x in (the Sorts of U1).s1 & y in (the Sorts of U1).s1; reconsider x1 = x, y1 = y as Element of (the Sorts of U1).s1 by A4; S1.s3 c= S1.s4 by A3,OSALG_1:def 16; then reconsider x2 = x, y2 = y as Element of (the Sorts of U1).s2 by A4; A5: [x2,y2] in MSCng(F,s2) iff (F.s2).x2 = (F.s2).y2 by MSUALG_4:def 17; dom (F.s3) = S1.s3 by FUNCT_2:def 1; then A6: (F.s3).x1 = (F.s4).x1 & (F.s3).y1 = (F.s4).y1 by A2,A3,OSALG_3:def 1; (MSCng(F)).s1 = MSCng(F,s1) by A1,MSUALG_4:def 18; hence [x,y] in (MSCng(F)).s1 iff [x,y] in (MSCng(F)).s2 by A1,A5,A6, MSUALG_4:def 17,def 18; end; hence thesis by Def2; 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 :Def23: MSCng(F); correctness by A1,Th16; 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 that A1: F is_homomorphism U1,U2 and A2: F is order-sorted; func OSHomQuot(F,s) -> Function of (the Sorts of (QuotOSAlg (U1,OSCng F))).s ,(the Sorts of U2).s means :Def24: 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; defpred P[set,set] means for a be Element of S1.s st $1 = OSClass(OSCng(F) ,a) holds $2 = (F.s).a; A3: cqa.s = OSClass (OSCng(F),s) by Def11; A4: 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 A5: a in (the Sorts of U1).s and A6: x = Class( CompClass(OSCng(F),CComp(s)), a) by A3,Def10; reconsider a as Element of S1.s by A5; take y = (F.s).a; thus y in S2.s; let b be Element of S1.s; assume A7: x = OSClass(OSCng(F),b); x = OSClass(OSCng(F),a) by A6; then [b,a] in (OSCng(F)).s by A7,Th12; then [b,a] in (MSCng(F)).s by A1,A2,Def23; then [b,a] in MSCng(F,s) by A1,MSUALG_4:def 18; hence thesis by MSUALG_4:def 17; end; consider G being Function such that A8: dom G = cqa.s & rng G c= S2.s & for x be set st x in cqa.s holds P[x,G.x] from FUNCT_1:sch 5(A4); reconsider G as Function of cqa.s,S2.s by A8,FUNCT_2:def 1,RELSET_1:4; take G; let a be Element of S1.s; thus thesis by A3,A8; end; uniqueness proof set qa = QuotOSAlg (U1, OSCng F), cqa = the Sorts of qa, u1 = the Sorts of U1, u2 = the Sorts of U2; let H,G be Function of cqa.s,u2.s; assume that A9: for a be Element of u1.s holds H.(OSClass(OSCng(F),a)) = (F.s).a and A10: for a be Element of u1.s holds G.(OSClass(OSCng(F),a)) = (F.s).a; A11: cqa.s = OSClass (OSCng(F),s) by Def11; 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 A12: y in (the Sorts of U1).s and A13: x = Class( CompClass(OSCng(F),CComp(s)), y) by A11,Def10; reconsider y1 = y as Element of u1.s by A12; A14: OSClass(OSCng(F),y1) = x by A13; hence H.x = (F.s).y1 by A9 .= G.x by A10,A14; end; hence thesis by FUNCT_2:12; 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 :Def25: 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 FUNCT_1:sch 4; reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2 ,RELAT_1:def 18; 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; f.y = OSHomQuot(F,y) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6; 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 PBOOLE:def 15; 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) by A2; hence H.i = G.i by A3; end; hence thesis by PBOOLE:3; end; end; theorem Th17: 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 that A1: F is_homomorphism U1,U2 and A2: F is order-sorted; for o be Element of the carrier' 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 carrier' 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: dom x = dom ar by MSUALG_3:6; Args(o,qa) = ((OSClass mc)# * (the Arity of S)).o by MSUALG_1:def 4; then consider a be Element of Args(o,U1) such that A4: x = mc #_os a by Th14; A5: dom a = dom ar by MSUALG_3:6; A6: now let y be set; assume A7: y in dom ar; then reconsider n = y as Nat; ar.n in rng ar by A7,FUNCT_1:def 3; then reconsider s = ar.n as SortSymbol of S; A8: ar/.n = ar.n by A7,PARTFUN1:def 6; then consider an being Element of S1.s such that A9: an = a.n and A10: x.n = OSClass(mc,an) by A4,A7,Def13; (qh # x).n = (qh.s).(x.n) by A3,A7,A8,MSUALG_3:def 6 .= OSHomQuot(F,s).OSClass(mc,an) by A10,Def25 .= (F.s).an by A1,A2,Def24 .= (F # a).n by A5,A7,A8,A9,MSUALG_3:def 6; hence (qh # x).y = (F # a).y; end; o in the carrier' of S; then o in dom (S1 * the ResultSort of S) by PARTFUN1:def 2; then A11: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the ResultSort of S).o) by FUNCT_1:12 .= (the Sorts of U1).ro by MSUALG_1:def 2; then rng Den(o,U1) c= Result(o,U1) & Result(o,U1) = S1.ro by MSUALG_1:def 5 ; then rng Den(o,U1) c= dom OSQuotRes(mc,o) by A11,FUNCT_2:def 1; then A12: dom Den(o,U1) = Args(o,U1) & dom ((OSQuotRes(mc,o)) * Den(o,U1)) = dom Den(o,U1) by FUNCT_2:def 1,RELAT_1:27; ar = (the Arity of S).o by MSUALG_1:def 1; then A13: product((OSClass mc) * ar) = ((OSClass mc)# * the Arity of S).o by MSAFREE:1; reconsider da = (Den(o,U1)).a as Element of S1.ro by A11,MSUALG_1:def 5; A14: qh.ro = OSHomQuot(F,ro) by Def25; Den(o,qa) = (OSQuotCharact mc).o by MSUALG_1:def 6 .= OSQuotCharact(mc,o1) by Def19; then Den(o,qa).x = (OSQuotRes(mc,o) * Den(o,U1)).a by A4,A13,Def18 .= (OSQuotRes(mc,o)) . da by A12,FUNCT_1:12 .= OSClass (OSCng(F),da) by Def14; then A15: (qh.ro).(Den(o,qa).x) = (F.ro).((Den(o,U1)).a) by A1,A2,A14,Def24 .= Den(o,U2).(F#a) by A1,MSUALG_3:def 7; dom (qh # x) = dom ar & dom (F # a) = dom ar by MSUALG_3:6; hence thesis by A6,A15,FUNCT_1:2; end; hence qh is_homomorphism qa,U2 by MSUALG_3:def 7; 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; A16: f = OSHomQuot(F,s) by Def25; 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 that A17: x1 in dom f and A18: x2 in dom f and A19: f.x1 = f.x2; x2 in (OSClass mc).s by A16,A18,FUNCT_2:def 1; then x2 in OSClass (mc,s) by Def11; then consider a2 being set such that A20: a2 in S1.s and A21: x2 = Class( CompClass(OSCng(F),CComp(s)), a2) by Def10; reconsider a2 as Element of S1.s by A20; A22: x2 = OSClass(OSCng(F),a2) by A21; x1 in (OSClass mc).s by A16,A17,FUNCT_2:def 1; then x1 in OSClass (mc,s) by Def11; then consider a1 being set such that A23: a1 in S1.s and A24: x1 = Class( CompClass(OSCng(F),CComp(s)), a1) by Def10; reconsider a1 as Element of S1.s by A23; (F.s).a1 = f.(OSClass(OSCng(F),a1)) & (F.s).a2 = f.(OSClass(OSCng(F ),a2)) by A1,A2,A16,Def24; then [a1,a2] in MSCng(F,s) by A19,A24,A21,MSUALG_4:def 17; then [a1,a2] in (MSCng(F)).s by A1,MSUALG_4:def 18; then A25: [a1,a2] in (OSCng(F)).s by A1,A2,Def23; x1 = OSClass(OSCng(F),a1) by A24; hence thesis by A22,A25,Th12; end; hence thesis by FUNCT_1:def 4; end; hence qh is "1-1" by MSUALG_3:1; thus OSHomQuot(F) is order-sorted proof reconsider S1O = S1 as OrderSortedSet of S by OSALG_1:17; reconsider sqa = the Sorts of qa as OrderSortedSet of S; let s1,s2 being Element of S such that A26: s1 <= s2; let a1 be set such that A27: a1 in dom (qh.s1); a1 in (OSClass OSCng(F)).s1 by A27; then a1 in OSClass (OSCng(F),s1) by Def11; then consider x being set such that A28: x in S1.s1 and A29: a1 = Class( CompClass(OSCng(F),CComp(s1)), x) by Def10; S1O.s1 c= S1O.s2 by A26,OSALG_1:def 16; then reconsider x2 = x as Element of S1.s2 by A28; A30: a1 = OSClass(OSCng(F),x2) by A26,A29,Th4; reconsider s3 = s1, s4 = s2 as Element of S; A31: dom (qh.s1) = (the Sorts of qa).s1 & dom (qh.s2) = (the Sorts of qa). s2 by FUNCT_2:def 1; reconsider x1 = x as Element of S1.s1 by A28; x1 in dom (F.s3) by A28,FUNCT_2:def 1; then A32: (F.s3).x1 = (F.s4).x1 by A2,A26,OSALG_3:def 1; sqa.s1 c= sqa.s2 by A26,OSALG_1:def 16; hence a1 in dom (qh.s2) by A27,A31; thus (qh.s1).a1 = OSHomQuot(F,s1).(OSClass(OSCng(F),x1)) by A29,Def25 .= (F.s2).x1 by A1,A2,A32,Def24 .= OSHomQuot(F,s2).(OSClass(OSCng(F),x2)) by A1,A2,Def24 .= (qh.s2).a1 by A30,Def25; end; end; theorem Th18: 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 that A1: F is_epimorphism U1,U2 and A2: F is order-sorted; set Sq = the Sorts of qa, S1 = the Sorts of U1, S2 = the Sorts of U2; A3: F is_homomorphism U1,U2 by A1,MSUALG_3:def 8; A4: F is "onto" by A1,MSUALG_3:def 8; 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; A5: rng (F.s) = S2.s by A4,MSUALG_3:def 3; A6: qh.i = OSHomQuot(F,s) by Def25; then A7: dom f = Sq.s by FUNCT_2:def 1; thus rng f c= S2.i by A6,RELAT_1:def 19; let x be set; assume x in S2.i; then consider a be set such that A8: a in dom (F.s) and A9: (F.s).a = x by A5,FUNCT_1:def 3; A10: Sq.s = OSClass (OSCng(F),s) by Def11; reconsider a as Element of S1.s by A8; f.(OSClass(OSCng(F),a)) = x by A2,A3,A6,A9,Def24; hence thesis by A7,A10,FUNCT_1:def 3; end; then A11: qh is "onto" by MSUALG_3:def 3; qh is_monomorphism qa,U2 by A2,A3,Th17; then qh is_homomorphism qa,U2 & qh is "1-1" by MSUALG_3:def 9; hence thesis by A11,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 Th18; hence thesis by MSUALG_3:def 11; 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 :Def26: 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 Th20: 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:18; C is os-compatible proof reconsider O1 = (the Sorts of U1) as OrderSortedSet of S by OSALG_1:17; let s1,s2 be Element of S such that A1: s1 <= s2; reconsider s3 = s1, s4 = s2 as Element of S; A2: O1.s3 c= O1.s4 by A1,OSALG_1:def 16; A3: 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 PBOOLE:def 16; let x,y be set; assume x in (the Sorts of U1).s1 & y in (the Sorts of U1).s1; hence [x,y] in C.s1 iff [x,y] in C.s2 by A2,A3,ZFMISC_1:87; end; hence thesis by Def2; end; theorem Th21: 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) |]; 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; set s2 = the_result_sort_of o2, s1 = the_result_sort_of o1; s1 <= s2 by A2,OSALG_1:def 20; then A3: O1.s1 c= O1.s2 by OSALG_1:def 16; 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); A4: Den(o1,U1).x1 in (the Sorts of U1).s1 & Den(o2,U1).x2 in (the Sorts of U1). s2 by MSUALG_9:18; R.s2 = [:(the Sorts of U1).s2,(the Sorts of U1).s2:] by A1,PBOOLE:def 16; hence thesis by A3,A4,ZFMISC_1:87; end; registration let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster monotone for OSCongruence of U1; existence proof reconsider R = [| the Sorts of U1, the Sorts of U1 |] as OSCongruence of U1 by Th20; take R; thus thesis by Th21; end; end; registration let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster monotone for MSEquivalence-like OrderSortedRelation of U1; existence proof set R = the monotone OSCongruence of U1; take R; thus thesis; end; end; theorem Th22: 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 carrier' 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 Def26; hence thesis by MSUALG_4:def 4; end; registration let S be OrderSortedSign, U1 be non-empty OSAlgebra of S; cluster monotone -> MSCongruence-like for MSEquivalence-like OrderSortedRelation of U1; coherence by Th22; end; theorem Th23: 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); 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; let x2 be Element of Args(o2,U1); assume for y being Nat st y in dom x1 holds [x1.y,x2.y] in R.((the_arity_of o2)/.y); then A2: [Den(o2,U1).x3,Den(o2,U1).x2] in R.(the_result_sort_of o2) by MSUALG_4:def 4; x1 in Args(o1,U1); then A3: x1 in dom Den(o1,U1) by FUNCT_2:def 1; Den(o1,U1) c= Den(o2,U1) by A1,OSALG_1:27; hence thesis by A2,A3,GRFUNC_1:2; end; registration let S be OrderSortedSign, U1 be monotone non-empty OSAlgebra of S; cluster -> monotone for OSCongruence of U1; coherence by Th23; end; :: monotonicity of quotient by monotone oscongruence registration let S; let U1 be non-empty OSAlgebra of S; let R be monotone OSCongruence of U1; cluster QuotOSAlg(U1,R) -> monotone; coherence proof reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; set A = QuotOSAlg(U1,R); let o1,o2 be OperSymbol of S such that A1: o1 <= o2; A2: Args(o1,A) c= Args(o2,A) by A1,OSALG_1:26; Den(o2,A) = (OSQuotCharact R).o2 by MSUALG_1:def 6; then A3: Den(o2,A) = OSQuotCharact( R,o2) by Def19; o2 in the carrier' of S; then A4: o2 in dom (the ResultSort of S) by FUNCT_2:def 1; Den(o1,A) = (OSQuotCharact R).o1 by MSUALG_1:def 6; then A5: Den(o1,A) = OSQuotCharact( R,o1) by Def19; o1 in the carrier' of S; then A6: o1 in dom (the ResultSort of S) by FUNCT_2:def 1; A7: (the_arity_of o1) <= (the_arity_of o2) by A1,OSALG_1:def 20; then len (the_arity_of o1) = len (the_arity_of o2) by OSALG_1:def 6; then A8: dom (the_arity_of o1) = dom (the_arity_of o2) by FINSEQ_3:29; A9: the_result_sort_of o1 <= the_result_sort_of o2 by A1,OSALG_1:def 20; then A10: O1.(the_result_sort_of o1) c= O1.(the_result_sort_of o2) by OSALG_1:def 17 ; A11: 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; assume x in dom Den(o1,A); then A12: x in Args(o1,A); then A13: x in ((OSClass R)# * the Arity of S).o1 by MSUALG_1:def 4; then consider a1 being Element of Args(o1,U1) such that A14: x = R #_os a1 by Th14; Result(o1,U1) = ((the Sorts of U1) * the ResultSort of S).o1 by MSUALG_1:def 5 .= (the Sorts of U1).((the ResultSort of S).o1) by A6,FUNCT_1:13 .= (the Sorts of U1).(the_result_sort_of o1) by MSUALG_1:def 2; then reconsider da1 = Den(o1,U1).a1 as Element of (the Sorts of U1).( the_result_sort_of o1); reconsider da12 = da1 as Element of (the Sorts of U1).( the_result_sort_of o2) by A10,TARSKI:def 3; a1 in Args(o1,U1); then a1 in dom Den(o1,U1) by FUNCT_2:def 1; then A15: ((OSQuotRes(R,o1)) * (Den(o1,U1))).a1 = OSQuotRes(R,o1).da1 by FUNCT_1:13 .= OSClass(R,da1) by Def14; A16: OSQuotCharact(R,o1).(R #_os a1) = ((OSQuotRes(R,o1)) * (Den(o1,U1)) ).a1 by A13,A14,Def18; x in Args(o2,A) by A2,A12; then A17: x in ((OSClass R)# * the Arity of S).o2 by MSUALG_1:def 4; then consider a2 being Element of Args(o2,U1) such that A18: x = R #_os a2 by Th14; 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 A19: y in dom a1; A20: y in dom (the_arity_of o1) by A19,MSUALG_6:2; then consider z1 being Element of (the Sorts of U1).((the_arity_of o1)/.y ) such that A21: z1 = a1.y and A22: (R #_os a1).y = OSClass(R, z1) by Def13; reconsider s1 = (the_arity_of o1).y, s2 = (the_arity_of o2).y as SortSymbol of S by A8,A20,PARTFUN1:4; A23: y in dom (the_arity_of o2) by A8,A19,MSUALG_6:2; then A24: (the_arity_of o2)/.y = (the_arity_of o2).y by PARTFUN1:def 6; A25: (the_arity_of o1)/.y = (the_arity_of o1).y & s1 <= s2 by A7,A20, OSALG_1:def 6,PARTFUN1:def 6; then (the Sorts of U1).((the_arity_of o1)/.y) c= (the Sorts of U1).(( the_arity_of o2)/.y) by A24,OSALG_1:def 17; then reconsider z12 = z1 as Element of (the Sorts of U1).((the_arity_of o2) /.y) by TARSKI:def 3; consider z2 being Element of (the Sorts of U1).((the_arity_of o2)/.y) such that A26: z2 = a2.y and A27: (R #_os a2).y = OSClass(R, z2) by A23,Def13; OSClass(R, z2) = OSClass(R, z12) by A14,A18,A22,A27,A24,A25,Th4; hence thesis by A21,A26,Th12; end; then A28: [Den(o1,U1).a1,Den(o2,U1).a2] in R.(the_result_sort_of o2) by A1,Def26; Result(o2,U1) = ((the Sorts of U1) * the ResultSort of S).o2 by MSUALG_1:def 5 .= (the Sorts of U1).((the ResultSort of S).o2) by A4,FUNCT_1:13 .= (the Sorts of U1).(the_result_sort_of o2) by MSUALG_1:def 2; 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 A29: ((OSQuotRes(R,o2)) * (Den(o2,U1))).a2 = OSQuotRes(R,o2).da2 by FUNCT_1:13 .= OSClass(R,da2) by Def14; OSClass(R,da1) = OSClass(R,da12) by A9,Th4 .= OSClass(R,da2) by A28,Th12; hence thesis by A5,A3,A17,A14,A18,A16,A15,A29,Def18; end; dom Den(o2,A) = Args(o2,A) & dom Den(o1,A) = Args(o1,A) by FUNCT_2:def 1; then dom Den(o1,A) = (dom Den(o2,A)) /\ Args(o1,A) by A2,XBOOLE_1:28; hence thesis by A11,FUNCT_1:46; end; end; 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 and A2: F is order-sorted; reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; set O1 = the Sorts of U1; let o1,o2 being OperSymbol of S such that A3: o1 <= o2; A4: Den(o2,U2)|Args(o1,U2) = Den(o1,U2) by A3,OSALG_1:def 21; set R = OSCng(F), 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 A5: for y being Nat st y in dom x1 holds [x1.y,x2.y] in R.((the_arity_of o2)/.y); Args(o1,U1) c= Args(o2,U1) by A3,OSALG_1:26; then reconsider x12=x1 as Element of Args(o2,U1) by TARSKI:def 3; set D1 = Den(o1,U1).x1, D2 = Den(o2,U1).x2, M = MSCng(F); A6: D1 in S1.rs1 by MSUALG_9:18; F#x1 in Args(o1,U2); then A7: F#x1 in dom Den(o1,U2) by FUNCT_2:def 1; A8: rs1 <= rs2 by A3,OSALG_1:def 20; then S1.rs1 c= S1.rs2 by OSALG_1:def 16; then reconsider D11=D1,D12=Den(o2,U1).x12 as Element of O1.rs2 by A6, MSUALG_9:18; D1 in dom (F.rs1) by A6,FUNCT_2:def 1; then (F.rs2).(Den(o1,U1).x1) = (F.rs1).(Den(o1,U1).x1) by A2,A8,OSALG_3:def 1 .= Den(o1,U2).(F#x1) by A1,MSUALG_3:def 7 .= Den(o2,U2).(F#x1) by A7,A4,FUNCT_1:47 .= Den(o2,U2).(F#x12) by A2,A3,OSALG_3:12 .= (F.rs2).(Den(o2,U1).x12) by A1,MSUALG_3:def 7; then A9: D2 in O1.rs2 & [D11,D12] in MSCng(F,rs2) by MSUALG_4:def 17,MSUALG_9:18; field(R.rs2) = (O1.rs2) by ORDERS_1:12; then A10: (R.rs2) is_transitive_in (O1.rs2) by RELAT_2:def 16; A11: [Den(o2,U1).x12,Den(o2,U1).x2] in R.rs2 by A5,MSUALG_4:def 4; M.rs2 = MSCng(F,rs2) & M = R by A1,A2,Def23,MSUALG_4:def 18; hence thesis by A11,A9,A10,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 that A1: F is_homomorphism U1,U2 and A2: F is order-sorted and A3: R c= OSCng F; func OSHomQuot(F,R,s) -> Function of (the Sorts of (QuotOSAlg (U1,R))).s,( the Sorts of U2).s means :Def27: 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; defpred P[set,set] means for a be Element of S1.s st $1 = OSClass(R,a) holds $2 = (F.s).a; A4: cqa.s = OSClass (R,s) by Def11; A5: 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; A6: R.s c= (OSCng F).s by A3,PBOOLE:def 2; assume x in cqa.s; then consider a being set such that A7: a in (the Sorts of U1).s and A8: x = Class( CompClass(R,CComp(s)), a) by A4,Def10; reconsider a as Element of S1.s by A7; take y = (F.s).a; thus y in S2.s; let b be Element of S1.s; assume A9: x = OSClass(R,b); x = OSClass(R,a) by A8; then [b,a] in R.s by A9,Th12; then [b,a] in (OSCng(F)).s by A6; then [b,a] in (MSCng(F)).s by A1,A2,Def23; then [b,a] in MSCng(F,s) by A1,MSUALG_4:def 18; hence thesis by MSUALG_4:def 17; end; consider G being Function such that A10: dom G = cqa.s & rng G c= S2.s & for x be set st x in cqa.s holds P[x,G.x] from FUNCT_1:sch 5(A5); reconsider G as Function of cqa.s,S2.s by A10,FUNCT_2:def 1,RELSET_1:4; take G; let a be Element of S1.s; thus thesis by A4,A10; end; uniqueness proof set qa = QuotOSAlg (U1, R), cqa = the Sorts of qa, u1 = the Sorts of U1, u2 = the Sorts of U2; let H,G be Function of cqa.s,u2.s; assume that A11: for a be Element of u1.s holds H.(OSClass(R,a)) = (F.s).a and A12: for a be Element of u1.s holds G.(OSClass(R,a)) = (F.s).a; A13: cqa.s = OSClass (R,s) by Def11; 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 A14: y in (the Sorts of U1).s and A15: x = Class( CompClass(R,CComp(s)), y) by A13,Def10; reconsider y1 = y as Element of u1.s by A14; A16: OSClass(R,y1) = x by A15; hence H.x = (F.s).y1 by A11 .= G.x by A12,A16; end; hence thesis by FUNCT_2:12; 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 : Def28: 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 FUNCT_1:sch 4; reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2 ,RELAT_1:def 18; 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; f.y = OSHomQuot(F,R,y) by A1; hence thesis; end; then reconsider f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6; 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 PBOOLE:def 15; 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) by A2; hence H.i = G . i by A3; 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 that A1: F is_homomorphism U1,U2 and A2: F is order-sorted and A3: R c= OSCng F; for o be Element of the carrier' 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 carrier' 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; A4: dom x = dom ar by MSUALG_3:6; Args(o,qa) = ((OSClass mc)# * (the Arity of S)).o by MSUALG_1:def 4; then consider a be Element of Args(o,U1) such that A5: x = mc #_os a by Th14; A6: dom a = dom ar by MSUALG_3:6; A7: now let y be set; assume A8: y in dom ar; then reconsider n = y as Nat; ar.n in rng ar by A8,FUNCT_1:def 3; then reconsider s = ar.n as SortSymbol of S; A9: ar/.n = ar.n by A8,PARTFUN1:def 6; then consider an being Element of S1.s such that A10: an = a.n and A11: x.n = OSClass(mc,an) by A5,A8,Def13; (qh # x).n = (qh.s).(x.n) by A4,A8,A9,MSUALG_3:def 6 .= OSHomQuot(F,R,s).OSClass(mc,an) by A11,Def28 .= (F.s).an by A1,A2,A3,Def27 .= (F # a).n by A6,A8,A9,A10,MSUALG_3:def 6; hence (qh # x).y = (F # a).y; end; o in the carrier' of S; then o in dom (S1 * the ResultSort of S) by PARTFUN1:def 2; then A12: ((the Sorts of U1) * the ResultSort of S).o = (the Sorts of U1).((the ResultSort of S).o) by FUNCT_1:12 .= (the Sorts of U1).ro by MSUALG_1:def 2; then rng Den(o,U1) c= Result(o,U1) & Result(o,U1) = S1.ro by MSUALG_1:def 5 ; then rng Den(o,U1) c= dom OSQuotRes(mc,o) by A12,FUNCT_2:def 1; then A13: dom Den(o,U1) = Args(o,U1) & dom ((OSQuotRes(mc,o)) * Den(o,U1)) = dom Den(o,U1) by FUNCT_2:def 1,RELAT_1:27; ar = (the Arity of S).o by MSUALG_1:def 1; then A14: product((OSClass mc) * ar) = ((OSClass mc)# * the Arity of S).o by MSAFREE:1; reconsider da = (Den(o,U1)).a as Element of S1.ro by A12,MSUALG_1:def 5; A15: qh.ro = OSHomQuot(F,R,ro) by Def28; Den(o,qa) = (OSQuotCharact mc).o by MSUALG_1:def 6 .= OSQuotCharact(mc,o1) by Def19; then Den(o,qa).x = (OSQuotRes(mc,o) * Den(o,U1)).a by A5,A14,Def18 .= (OSQuotRes(mc,o)) . da by A13,FUNCT_1:12 .= OSClass (R,da) by Def14; then A16: (qh.ro).(Den(o,qa).x) = (F.ro).((Den(o,U1)).a) by A1,A2,A3,A15,Def27 .= Den(o,U2).(F#a) by A1,MSUALG_3:def 7; dom (qh # x) = dom ar & dom (F # a) = dom ar by MSUALG_3:6; hence thesis by A7,A16,FUNCT_1:2; end; hence qh is_homomorphism qa,U2 by MSUALG_3:def 7; thus OSHomQuot(F,R) is order-sorted proof reconsider S1O = S1 as OrderSortedSet of S by OSALG_1:17; reconsider sqa = the Sorts of qa as OrderSortedSet of S; let s1,s2 being Element of S such that A17: s1 <= s2; let a1 be set such that A18: a1 in dom (qh.s1); a1 in (OSClass R).s1 by A18; then a1 in OSClass (R,s1) by Def11; then consider x being set such that A19: x in S1.s1 and A20: a1 = Class( CompClass(R,CComp(s1)), x) by Def10; S1O.s1 c= S1O.s2 by A17,OSALG_1:def 16; then reconsider x2 = x as Element of S1.s2 by A19; A21: a1 = OSClass(R,x2) by A17,A20,Th4; reconsider s3 = s1, s4 = s2 as Element of S; A22: dom (qh.s1) = (the Sorts of qa).s1 & dom (qh.s2) = (the Sorts of qa). s2 by FUNCT_2:def 1; reconsider x1 = x as Element of S1.s1 by A19; x1 in dom (F.s3) by A19,FUNCT_2:def 1; then A23: (F.s3).x1 = (F.s4).x1 by A2,A17,OSALG_3:def 1; sqa.s1 c= sqa.s2 by A17,OSALG_1:def 16; hence a1 in dom (qh.s2) by A18,A22; thus (qh.s1).a1 = OSHomQuot(F,R,s1).(OSClass(R,x1)) by A20,Def28 .= (F.s2).x1 by A1,A2,A3,A23,Def27 .= OSHomQuot(F,R,s2).(OSClass(R,x2)) by A1,A2,A3,Def27 .= (qh.s2).a1 by A21,Def28; end; end;