:: OSALG_4 semantic presentation begin registration let R be non empty Poset; cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding order-sorted for set ; existence ex b1 being OrderSortedSet of R st b1 is Relation-yielding proof set R1 = the Relation; set I = the carrier of R; set f = the carrier of R --> the Relation; reconsider f = the carrier of R --> the Relation as ManySortedSet of the carrier of R ; f is order-sorted proof let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or f . s1 c= f . s2 ) assume s1 <= s2 ; ::_thesis: f . s1 c= f . s2 f . s1 = the Relation by FUNCOP_1:7; hence f . s1 c= f . s2 by FUNCOP_1:7; ::_thesis: verum end; then reconsider f = f as OrderSortedSet of R ; take f ; ::_thesis: f is Relation-yielding for x being set st x in dom f holds f . x is Relation by FUNCOP_1:7; hence f is Relation-yielding by FUNCOP_1:def_11; ::_thesis: verum end; end; definition let R be non empty Poset; let A, B be ManySortedSet of the carrier of R; let IT be ManySortedRelation of A,B; attrIT is os-compatible means :Def1: :: OSALG_4:def 1 for s1, s2 being Element of R st s1 <= s2 holds 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; :: deftheorem Def1 defines os-compatible OSALG_4:def_1_:_ for R being non empty Poset for A, B being ManySortedSet of the carrier of R for IT being ManySortedRelation of A,B holds ( IT is os-compatible iff for s1, s2 being Element of R st s1 <= s2 holds 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 ) ); registration let R be non empty Poset; let A, B be ManySortedSet of the carrier of R; cluster non empty Relation-like the carrier of R -defined Function-like total Relation-yielding os-compatible for ManySortedRelation of A,B; existence ex b1 being ManySortedRelation of A,B st b1 is os-compatible proof set I = the carrier of R; consider R1 being Relation such that A1: R1 = {} ; set f = the carrier of R --> R1; reconsider f = the carrier of R --> R1 as ManySortedSet of R ; set f1 = f; for i being set st i in the carrier of R holds f . i is Relation of (A . i),(B . i) proof let i be set ; ::_thesis: ( i in the carrier of R implies f . i is Relation of (A . i),(B . i) ) assume i in the carrier of R ; ::_thesis: f . i is Relation of (A . i),(B . i) then f . i = {} by A1, FUNCOP_1:7; hence f . i is Relation of (A . i),(B . i) by RELSET_1:12; ::_thesis: verum end; then reconsider f2 = f as ManySortedRelation of A,B by MSUALG_4:def_1; take f ; ::_thesis: ( f is ManySortedRelation of A,B & f is os-compatible ) for s1, s2 being Element of R st s1 <= s2 holds for x, y being set st x in A . s1 & y in B . s1 holds ( [x,y] in f . s1 iff [x,y] in f . s2 ) proof let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies for x, y being set st x in A . s1 & y in B . s1 holds ( [x,y] in f . s1 iff [x,y] in f . s2 ) ) assume s1 <= s2 ; ::_thesis: for x, y being set st x in A . s1 & y in B . s1 holds ( [x,y] in f . s1 iff [x,y] in f . s2 ) let x, y be set ; ::_thesis: ( x in A . s1 & y in B . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) ) assume that x in A . s1 and y in B . s1 ; ::_thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 ) f . s1 = R1 by FUNCOP_1:7 .= f . s2 by FUNCOP_1:7 ; hence ( [x,y] in f . s1 iff [x,y] in f . s2 ) ; ::_thesis: verum end; then f2 is os-compatible by Def1; hence ( f is ManySortedRelation of A,B & f is os-compatible ) ; ::_thesis: verum 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: :: OSALG_4:1 for R being non empty Poset for A, B being ManySortedSet of the carrier of R for OR being ManySortedRelation of A,B st OR is os-compatible holds OR is OrderSortedSet of R proof let R be non empty Poset; ::_thesis: for A, B being ManySortedSet of the carrier of R for OR being ManySortedRelation of A,B st OR is os-compatible holds OR is OrderSortedSet of R let A, B be ManySortedSet of the carrier of R; ::_thesis: for OR being ManySortedRelation of A,B st OR is os-compatible holds OR is OrderSortedSet of R let OR be ManySortedRelation of A,B; ::_thesis: ( OR is os-compatible implies OR is OrderSortedSet of R ) set OR1 = OR; assume A1: OR is os-compatible ; ::_thesis: OR is OrderSortedSet of R OR is order-sorted proof let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or OR . s1 c= OR . s2 ) assume A2: s1 <= s2 ; ::_thesis: OR . s1 c= OR . s2 for x, y being set st [x,y] in OR . s1 holds [x,y] in OR . s2 proof let x, y be set ; ::_thesis: ( [x,y] in OR . s1 implies [x,y] in OR . s2 ) assume A3: [x,y] in OR . s1 ; ::_thesis: [x,y] in OR . s2 ( x in A . s1 & y in B . s1 ) by A3, ZFMISC_1:87; hence [x,y] in OR . s2 by A1, A2, A3, Def1; ::_thesis: verum end; hence OR . s1 c= OR . s2 by RELAT_1:def_3; ::_thesis: verum end; hence OR is OrderSortedSet of R ; ::_thesis: verum 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 for b1 being ManySortedRelation of A,B st b1 is os-compatible holds b1 is order-sorted 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; let U1 be OSAlgebra of S; mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means :Def2: :: OSALG_4:def 2 it is os-compatible ; existence ex b1 being ManySortedRelation of U1 st b1 is os-compatible proof reconsider Y = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; set X = the OrderSortedRelation of Y; reconsider X1 = the OrderSortedRelation of Y as ManySortedRelation of U1 ; take X1 ; ::_thesis: X1 is os-compatible thus X1 is os-compatible ; ::_thesis: verum end; end; :: deftheorem Def2 defines OrderSortedRelation OSALG_4:def_2_:_ for S being OrderSortedSign for U1 being OSAlgebra of S for b3 being ManySortedRelation of U1 holds ( b3 is OrderSortedRelation of U1 iff b3 is os-compatible ); registration let S be OrderSortedSign; let U1 be OSAlgebra of S; cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like for OrderSortedRelation of U1; existence ex b1 being OrderSortedRelation of U1 st b1 is MSEquivalence-like proof deffunc H1( Element of S) -> Element of bool [:( the Sorts of U1 . S),( the Sorts of U1 . S):] = id ( the Sorts of U1 . S); consider f being Function such that A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; for i being 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 ; ::_thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ) assume i in the carrier of S ; ::_thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) then f . i = id ( the Sorts of U1 . i) by A1; hence f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by MSUALG_4:def_1; reconsider f = f as ManySortedRelation of U1 ; set f1 = f; A2: f 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; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in f . s1 iff [x,y] in f . s2 ) ) assume A3: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in f . s1 iff [x,y] in f . s2 ) reconsider s3 = s1, s4 = s2 as Element of S ; let x, y be set ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) ) assume that A4: x in the Sorts of U1 . s1 and y in the Sorts of U1 . s1 ; ::_thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 ) A5: f . s1 = id (X . s1) by A1; A6: f . 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 f . s1 implies [x,y] in f . s2 ) by A5, A6; ::_thesis: ( [x,y] in f . s2 implies [x,y] in f . s1 ) assume [x,y] in f . s2 ; ::_thesis: [x,y] in f . s1 then x = y by A6, RELAT_1:def_10; hence [x,y] in f . s1 by A5, A4, RELAT_1:def_10; ::_thesis: verum end; take f ; ::_thesis: ( f is OrderSortedRelation of U1 & f is MSEquivalence-like ) for i being set for R being 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 ; ::_thesis: for R being 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) let R be Relation of ( the Sorts of U1 . i); ::_thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) ) assume ( i in the carrier of S & f . i = R ) ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i) then R = id ( the Sorts of U1 . i) by A1; hence R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum end; then f is MSEquivalence_Relation-like by MSUALG_4:def_2; hence ( f is OrderSortedRelation of U1 & f is MSEquivalence-like ) by A2, Def2, MSUALG_4:def_3; ::_thesis: verum end; end; registration let S be OrderSortedSign; let U1 be non-empty OSAlgebra of S; cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1; existence ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is MSCongruence-like proof deffunc H1( Element of S) -> Element of bool [:( the Sorts of U1 . S),( the Sorts of U1 . S):] = id ( the Sorts of U1 . S); consider f being Function such that A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; for i being 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 ; ::_thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ) assume i in the carrier of S ; ::_thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) then f . i = id ( the Sorts of U1 . i) by A1; hence f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by MSUALG_4:def_1; reconsider f = f as ManySortedRelation of U1 ; for i being set for R being 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 ; ::_thesis: for R being 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) let R be Relation of ( the Sorts of U1 . i); ::_thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) ) assume ( i in the carrier of S & f . i = R ) ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i) then R = id ( the Sorts of U1 . i) by A1; hence R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum end; then f is MSEquivalence_Relation-like by MSUALG_4:def_2; then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by MSUALG_4:def_3; set f1 = f; f 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; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in f . s1 iff [x,y] in f . s2 ) ) assume A2: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in f . s1 iff [x,y] in f . s2 ) reconsider s3 = s1, s4 = s2 as Element of S ; let x, y be set ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in f . s1 iff [x,y] in f . s2 ) ) assume that A3: x in the Sorts of U1 . s1 and y in the Sorts of U1 . s1 ; ::_thesis: ( [x,y] in f . s1 iff [x,y] in f . s2 ) A4: f . s1 = id (X . s1) by A1; A5: f . 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 f . s1 implies [x,y] in f . s2 ) by A4, A5; ::_thesis: ( [x,y] in f . s2 implies [x,y] in f . s1 ) assume [x,y] in f . s2 ; ::_thesis: [x,y] in f . s1 then x = y by A5, RELAT_1:def_10; hence [x,y] in f . s1 by A4, A3, RELAT_1:def_10; ::_thesis: verum end; then reconsider f = f as MSEquivalence-like OrderSortedRelation of U1 by Def2; take f ; ::_thesis: f is MSCongruence-like for o being Element of the carrier' of S for x, y being Element of Args (o,U1) st ( for n being 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; ::_thesis: for x, y being Element of Args (o,U1) st ( for n being 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) let x, y be Element of Args (o,U1); ::_thesis: ( ( for n being Nat st n in dom x holds [(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) implies [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) ) A6: dom x = dom (the_arity_of o) by MSUALG_3:6; assume A7: for n being Nat st n in dom x holds [(x . n),(y . n)] in f . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) A8: for a being 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 ; ::_thesis: ( a in dom (the_arity_of o) implies x . a = y . a ) assume A9: a in dom (the_arity_of o) ; ::_thesis: x . a = y . a then reconsider n = a as Nat ; (the_arity_of o) . n in rng (the_arity_of o) by A9, FUNCT_1:def_3; then A10: f . ((the_arity_of o) . n) = id ( the Sorts of U1 . ((the_arity_of o) . 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 . ((the_arity_of o) . n) by A7, A6, A9; hence x . a = y . a by A10, RELAT_1:def_10; ::_thesis: verum end; set r = the_result_sort_of o; A11: f . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) 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 . (the_result_sort_of o) 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 [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A11, A14, RELAT_1:def_10; ::_thesis: verum end; hence f is MSCongruence-like by MSUALG_4:def_4; ::_thesis: verum end; end; definition let S be OrderSortedSign; let U1 be non-empty OSAlgebra of S; mode OSCongruence of U1 is MSEquivalence-like MSCongruence-like OrderSortedRelation of U1; end; definition let R be non empty Poset; func Path_Rel R -> Equivalence_Relation of the carrier of R means :Def3: :: OSALG_4:def 3 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ); existence ex b1 being Equivalence_Relation of the carrier of R st for x, y being set holds ( [x,y] in b1 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) proof defpred S1[ 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(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 & S1[x,y] ) } ; { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } c= [: the carrier of R, the carrier of R:] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } or z in [: the carrier of R, the carrier of R:] ) assume z in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ; ::_thesis: z in [: the carrier of R, the carrier of R:] then ex x, y being Element of R st ( z = [x,y] & x in the carrier of R & y in the carrier of R & S1[x,y] ) ; hence z in [: the carrier of R, the carrier of R:] by ZFMISC_1:87; ::_thesis: verum end; then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } as Relation of the carrier of R ; A1: for x, y being set holds ( [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } iff ( x in the carrier of R & y in the carrier of R & S1[x,y] ) ) proof let x, y be set ; ::_thesis: ( [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } iff ( x in the carrier of R & y in the carrier of R & S1[x,y] ) ) hereby ::_thesis: ( x in the carrier of R & y in the carrier of R & S1[x,y] implies [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ) assume [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ; ::_thesis: ( x in the carrier of R & y in the carrier of R & S1[x,y] ) 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: S1[x1,y1] ; ( x = x1 & y = y1 ) by A2, XTUPLE_0:1; hence ( x in the carrier of R & y in the carrier of R & S1[x,y] ) by A3; ::_thesis: verum end; thus ( x in the carrier of R & y in the carrier of R & S1[x,y] implies [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ) ; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_set_st_x_in_the_carrier_of_R_&_y_in_the_carrier_of_R_&_[x,y]_in_P1_holds_ [y,x]_in_P1 let x, y be set ; ::_thesis: ( x in the carrier of R & y in the carrier of R & [x,y] in P1 implies [y,x] in P1 ) assume that A4: ( x in the carrier of R & y in the carrier of R ) and A5: [x,y] in P1 ; ::_thesis: [y,x] 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R by A1, A5; S1[y,x] proof take F = Rev p; ::_thesis: ( 1 < len F & F . 1 = y & F . (len F) = x & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds [(F . (n - 1)),(F . n)] in the InternalRel of R ) ) thus 1 < len F by A6, FINSEQ_5:def_3; ::_thesis: ( F . 1 = y & F . (len F) = x & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds [(F . (n - 1)),(F . n)] in the InternalRel of R ) ) A9: len F = len p by FINSEQ_5:def_3; hence ( F . 1 = y & F . (len F) = x ) by A7, FINSEQ_5:62; ::_thesis: for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds [(F . (n - 1)),(F . n)] in the InternalRel of R let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len F & not [(F . n1),(F . (n1 - 1))] in the InternalRel of R implies [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) assume that A10: 2 <= n1 and A11: n1 <= len F ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) 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 <= ((len p) - n1) + 2 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 ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A8, A15, A13, A16; ::_thesis: verum end; hence [y,x] in P1 by A4; ::_thesis: verum 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__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_R_holds_ [x,x]_in_P1 let x be set ; ::_thesis: ( x in the carrier of R implies [x,x] in P1 ) assume A19: x in the carrier of R ; ::_thesis: [x,x] in P1 S1[x,x] proof set F = <*x,x*>; rng <*x,x*> = {x,x} by FINSEQ_2:127 .= {x} by ENUMSET1:29 ; then rng <*x,x*> c= the carrier of R by A19, ZFMISC_1:31; then reconsider F1 = <*x,x*> as FinSequence of the carrier of R by FINSEQ_1:def_4; take F1 ; ::_thesis: ( 1 < len F1 & F1 . 1 = x & F1 . (len F1) = x & ( for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds [(F1 . (n - 1)),(F1 . n)] in the InternalRel of R ) ) A20: len <*x,x*> = 2 by FINSEQ_1:44; hence 1 < len F1 ; ::_thesis: ( F1 . 1 = x & F1 . (len F1) = x & ( for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds [(F1 . (n - 1)),(F1 . n)] in the InternalRel of R ) ) thus ( F1 . 1 = x & F1 . (len F1) = x ) by A20, FINSEQ_1:44; ::_thesis: for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds [(F1 . (n - 1)),(F1 . n)] in the InternalRel of R let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len F1 & not [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R implies [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R ) assume ( 2 <= n1 & n1 <= len F1 ) ; ::_thesis: ( [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R or [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R ) then A21: n1 = 2 by A20, XXREAL_0:1; ( <*x,x*> . 1 = x & <*x,x*> . 2 = x ) by FINSEQ_1:44; hence ( [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R or [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R ) by A18, A19, A21, RELAT_2:def_1; ::_thesis: verum end; hence [x,x] in P1 by A19; ::_thesis: verum 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__::_thesis:_for_x,_y,_z_being_set_st_x_in_the_carrier_of_R_&_y_in_the_carrier_of_R_&_z_in_the_carrier_of_R_&_[x,y]_in_P1_&_[y,z]_in_P1_holds_ [x,z]_in_P1 let x, y, z be set ; ::_thesis: ( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in P1 & [y,z] in P1 implies [x,z] in P1 ) 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 ) ; ::_thesis: [x,z] in P1 ( S1[x,y] & S1[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 & not [(p1 . n),(p1 . (n - 1))] in the InternalRel of R holds [(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 & not [(p2 . n),(p2 . (n - 1))] in the InternalRel of R holds [(p2 . (n - 1)),(p2 . n)] in the InternalRel of R ; S1[x,z] proof take F = p1 ^ p2; ::_thesis: ( 1 < len F & F . 1 = x & F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds [(F . (n - 1)),(F . n)] in the InternalRel of R ) ) 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; ::_thesis: ( F . 1 = x & F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds [(F . (n - 1)),(F . n)] in the InternalRel of R ) ) 1 in dom p1 by A27, FINSEQ_3:25; hence F . 1 = x by A28, FINSEQ_1:def_7; ::_thesis: ( F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds [(F . (n - 1)),(F . n)] in the InternalRel of R ) ) len p2 in dom p2 by A31, FINSEQ_3:25; hence F . (len F) = z by A33, A35, FINSEQ_1:def_7; ::_thesis: for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds [(F . (n - 1)),(F . n)] in the InternalRel of R let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len F & not [(F . n1),(F . (n1 - 1))] in the InternalRel of R implies [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) assume that A36: 2 <= n1 and A37: n1 <= len F ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) 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: ( not (len p1) + 1 <= n1 or (len p1) + 1 = n1 or (len p1) + 1 < n1 ) by XXREAL_0:1; A41: n1 - 1 <= (len F) - 0 by A37, XREAL_1:13; percases ( n1 <= len p1 or (len p1) + 1 < n1 or (len p1) + 1 = n1 ) by A40, INT_1:7; supposeA42: n1 <= len p1 ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) 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 ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A30, A36, A42, A43; ::_thesis: verum end; supposeA44: (len p1) + 1 < n1 ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) 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 ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A34, A46, A47, A48; ::_thesis: verum end; supposeA49: (len p1) + 1 = n1 ; ::_thesis: ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) ( (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 ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A18, A24, A50, RELAT_2:def_1; ::_thesis: verum end; end; end; hence [x,z] in P1 by A23, A25; ::_thesis: verum end; then P1 is_transitive_in the carrier of R by RELAT_2:def_8; then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } as Equivalence_Relation of the carrier of R by A22, A17, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; take P1 ; ::_thesis: for x, y being set holds ( [x,y] in P1 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) thus for x, y being set holds ( [x,y] in P1 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Equivalence_Relation of the carrier of R st ( for x, y being set holds ( [x,y] in b1 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) & ( for x, y being set holds ( [x,y] in b2 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) holds b1 = b2 proof let X, Y be Equivalence_Relation of the carrier of R; ::_thesis: ( ( for x, y being set holds ( [x,y] in X 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) & ( for x, y being set holds ( [x,y] in Y 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) implies X = Y ) defpred S1[ 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ); assume A51: for x, y being set holds ( [x,y] in X iff S1[x,y] ) ; ::_thesis: ( ex x, y being set st ( ( [x,y] in Y implies ( 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) implies ( 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) & not [x,y] in Y ) ) or X = Y ) assume A52: for x, y being set holds ( [x,y] in Y iff S1[x,y] ) ; ::_thesis: X = Y for x, y being set holds ( [x,y] in X iff [x,y] in Y ) proof let x, y be set ; ::_thesis: ( [x,y] in X iff [x,y] in Y ) hereby ::_thesis: ( [x,y] in Y implies [x,y] in X ) assume [x,y] in X ; ::_thesis: [x,y] in Y then S1[x,y] by A51; hence [x,y] in Y by A52; ::_thesis: verum end; assume [x,y] in Y ; ::_thesis: [x,y] in X then S1[x,y] by A52; hence [x,y] in X by A51; ::_thesis: verum end; hence X = Y by RELAT_1:def_2; ::_thesis: verum end; end; :: deftheorem Def3 defines Path_Rel OSALG_4:def_3_:_ for R being non empty Poset for b2 being Equivalence_Relation of the carrier of R holds ( b2 = Path_Rel R iff for x, y being set holds ( [x,y] in b2 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ); theorem Th2: :: OSALG_4:2 for R being non empty Poset for s1, s2 being Element of R st s1 <= s2 holds [s1,s2] in Path_Rel R proof let R be non empty Poset; ::_thesis: for s1, s2 being Element of R st s1 <= s2 holds [s1,s2] in Path_Rel R let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies [s1,s2] in Path_Rel R ) assume A1: s1 <= s2 ; ::_thesis: [s1,s2] in Path_Rel R set p = <*s1,s2*>; A2: len <*s1,s2*> = 2 by FINSEQ_1:44; A3: <*s1,s2*> . 1 = s1 by FINSEQ_1:44; A4: for n being Nat st 2 <= n & n <= len <*s1,s2*> & not [(<*s1,s2*> . n),(<*s1,s2*> . (n - 1))] in the InternalRel of R holds [(<*s1,s2*> . (n - 1)),(<*s1,s2*> . n)] in the InternalRel of R proof let n1 be Nat; ::_thesis: ( 2 <= n1 & n1 <= len <*s1,s2*> & not [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R implies [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R ) assume ( 2 <= n1 & n1 <= len <*s1,s2*> ) ; ::_thesis: ( [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R or [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R ) then A5: n1 = 2 by A2, XXREAL_0:1; [s1,s2] in the InternalRel of R by A1, ORDERS_2:def_5; hence ( [(<*s1,s2*> . n1),(<*s1,s2*> . (n1 - 1))] in the InternalRel of R or [(<*s1,s2*> . (n1 - 1)),(<*s1,s2*> . n1)] in the InternalRel of R ) by A3, A5, FINSEQ_1:44; ::_thesis: verum end; <*s1,s2*> . (len <*s1,s2*>) = s2 by A2, FINSEQ_1:44; hence [s1,s2] in Path_Rel R by A2, A3, A4, Def3; ::_thesis: verum end; definition let R be non empty Poset; let s1, s2 be Element of R; preds1 ~= s2 means :Def4: :: OSALG_4:def 4 [s1,s2] in Path_Rel R; reflexivity for s1 being Element of R holds [s1,s1] in Path_Rel R proof set PR = Path_Rel R; field (Path_Rel R) = the carrier of R by ORDERS_1:12; then Path_Rel R is_reflexive_in the carrier of R by RELAT_2:def_9; hence for s1 being Element of R holds [s1,s1] in Path_Rel R by RELAT_2:def_1; ::_thesis: verum end; symmetry for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds [s2,s1] in Path_Rel R proof set PR = Path_Rel R; field (Path_Rel R) = the carrier of R by ORDERS_1:12; then Path_Rel R is_symmetric_in the carrier of R by RELAT_2:def_11; hence for s1, s2 being Element of R st [s1,s2] in Path_Rel R holds [s2,s1] in Path_Rel R by RELAT_2:def_3; ::_thesis: verum end; end; :: deftheorem Def4 defines ~= OSALG_4:def_4_:_ for R being non empty Poset for s1, s2 being Element of R holds ( s1 ~= s2 iff [s1,s2] in Path_Rel R ); theorem :: OSALG_4:3 for R being non empty Poset for s1, s2, s3 being Element of R st s1 ~= s2 & s2 ~= s3 holds s1 ~= s3 proof let R be non empty Poset; ::_thesis: for s1, s2, s3 being Element of R st s1 ~= s2 & s2 ~= s3 holds s1 ~= s3 let s1, s2, s3 be Element of R; ::_thesis: ( s1 ~= s2 & s2 ~= s3 implies s1 ~= s3 ) set PR = Path_Rel R; field (Path_Rel R) = the carrier of R by ORDERS_1:12; then A1: Path_Rel R is_transitive_in the carrier of R by RELAT_2:def_16; assume ( s1 ~= s2 & s2 ~= s3 ) ; ::_thesis: s1 ~= s3 then ( [s1,s2] in Path_Rel R & [s2,s3] in Path_Rel R ) by Def4; then [s1,s3] in Path_Rel R by A1, RELAT_2:def_8; hence s1 ~= s3 by Def4; ::_thesis: verum end; definition let R be non empty Poset; func Components R -> non empty Subset-Family of R equals :: OSALG_4:def 5 Class (Path_Rel R); coherence Class (Path_Rel R) is non empty Subset-Family of R ; end; :: deftheorem defines Components OSALG_4:def_5_:_ for R being non empty Poset holds Components R = Class (Path_Rel R); registration let R be non empty Poset; cluster -> non empty for Element of Components R; coherence for b1 being Element of Components R holds not b1 is empty proof let X be Element of Components R; ::_thesis: not X is empty ex x being set st ( x in the carrier of R & X = Class ((Path_Rel R),x) ) by EQREL_1:def_3; hence not X is empty by EQREL_1:20; ::_thesis: verum 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 :: OSALG_4:def 6 Class ((Path_Rel R),s1); correctness coherence Class ((Path_Rel R),s1) is Component of R; by EQREL_1:def_3; end; :: deftheorem defines CComp OSALG_4:def_6_:_ for R being non empty Poset for s1 being Element of R holds CComp s1 = Class ((Path_Rel R),s1); theorem Th4: :: OSALG_4:4 for R being non empty Poset for s1, s2 being Element of R st s1 <= s2 holds CComp s1 = CComp s2 proof let R be non empty Poset; ::_thesis: for s1, s2 being Element of R st s1 <= s2 holds CComp s1 = CComp s2 let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies CComp s1 = CComp s2 ) assume s1 <= s2 ; ::_thesis: CComp s1 = CComp s2 then [s1,s2] in Path_Rel R by Th2; hence CComp s1 = CComp s2 by EQREL_1:35; ::_thesis: verum end; definition let R be non empty Poset; let A be ManySortedSet of the carrier of R; let C be Component of R; funcA -carrier_of C -> set equals :: OSALG_4:def 7 union { (A . s) where s is Element of R : s in C } ; correctness coherence union { (A . s) where s is Element of R : s in C } is set ; ; end; :: deftheorem defines -carrier_of OSALG_4:def_7_:_ for R being non empty Poset for A being ManySortedSet of the carrier of R for C being Component of R holds A -carrier_of C = union { (A . s) where s is Element of R : s in C } ; theorem Th5: :: OSALG_4:5 for R being non empty Poset for A being ManySortedSet of the carrier of R for s being Element of R for x being set st x in A . s holds x in A -carrier_of (CComp s) proof let R be non empty Poset; ::_thesis: for A being ManySortedSet of the carrier of R for s being Element of R for x being set st x in A . s holds x in A -carrier_of (CComp s) let A be ManySortedSet of the carrier of R; ::_thesis: for s being Element of R for x being set st x in A . s holds x in A -carrier_of (CComp s) let s be Element of R; ::_thesis: for x being set st x in A . s holds x in A -carrier_of (CComp s) let x be set ; ::_thesis: ( x in A . s implies x in A -carrier_of (CComp s) ) assume A1: x in A . s ; ::_thesis: x in A -carrier_of (CComp 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 x in A -carrier_of (CComp s) by A1, TARSKI:def_4; ::_thesis: verum end; definition let R be non empty Poset; attrR is locally_directed means :Def8: :: OSALG_4:def 8 for C being Component of R holds C is directed ; end; :: deftheorem Def8 defines locally_directed OSALG_4:def_8_:_ for R being non empty Poset holds ( R is locally_directed iff for C being Component of R holds C is directed ); theorem Th6: :: OSALG_4:6 for R being non empty discrete Poset for x, y being Element of R st [x,y] in Path_Rel R holds x = y proof let R be non empty discrete Poset; ::_thesis: for x, y being Element of R st [x,y] in Path_Rel R holds x = y let x, y be Element of R; ::_thesis: ( [x,y] in Path_Rel R implies x = y ) assume [x,y] in Path_Rel R ; ::_thesis: x = y 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 & not [(p . n),(p . (n - 1))] in the InternalRel of R holds [(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 S1[ Nat] means ( p . \$1 <> x & 1 <= \$1 ); let n1 be Nat; ::_thesis: ( 1 <= n1 & n1 <= len p implies p . n1 = x ) assume that A5: 1 <= n1 and A6: n1 <= len p ; ::_thesis: p . n1 = x assume A7: p . n1 <> x ; ::_thesis: contradiction then A8: ex k being Nat st S1[k] by A5; consider k being Nat such that A9: ( S1[k] & ( for n being Nat st S1[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; percases ( [pk,x] in the InternalRel of R or [x,pk] in the InternalRel of R ) by A4, A10, A13, A12; suppose [pk,x] in the InternalRel of R ; ::_thesis: contradiction then pk <= x by ORDERS_2:def_5; hence contradiction by A9, ORDERS_3:1; ::_thesis: verum end; suppose [x,pk] in the InternalRel of R ; ::_thesis: contradiction then x <= pk by ORDERS_2:def_5; hence contradiction by A9, ORDERS_3:1; ::_thesis: verum end; end; end; hence x = y by A1, A3; ::_thesis: verum end; theorem Th7: :: OSALG_4:7 for R being non empty discrete Poset for C being Component of R ex x being Element of R st C = {x} proof let R be non empty discrete Poset; ::_thesis: for C being Component of R ex x being Element of R st C = {x} let C be Component of R; ::_thesis: ex x being Element of R st C = {x} 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 ; ::_thesis: C = {x1} for y being set holds ( y in C iff y = x1 ) proof let y be set ; ::_thesis: ( y in C iff y = x1 ) hereby ::_thesis: ( y = x1 implies y in C ) assume A3: y in C ; ::_thesis: y = x1 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 ; ::_thesis: verum end; assume y = x1 ; ::_thesis: y in C hence y in C by A2, EQREL_1:20; ::_thesis: verum end; hence C = {x1} by TARSKI:def_1; ::_thesis: verum end; theorem Th8: :: OSALG_4:8 for R being non empty discrete Poset holds R is locally_directed proof let R be non empty discrete Poset; ::_thesis: R is locally_directed let C be Component of R; :: according to OSALG_4:def_8 ::_thesis: C is directed 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 holds ex z being Element of R st ( z in C & x <= z & y <= z ) proof let x1, y1 be Element of R; ::_thesis: ( x1 in C & y1 in C implies ex z being Element of R st ( z in C & x1 <= z & y1 <= z ) ) assume that A2: x1 in C and A3: y1 in C ; ::_thesis: ex z being Element of R st ( z in C & x1 <= z & y1 <= z ) take x1 ; ::_thesis: ( x1 in C & x1 <= x1 & y1 <= x1 ) x1 = x by A1, A2, TARSKI:def_1; hence ( x1 in C & x1 <= x1 & y1 <= x1 ) by A1, A3, TARSKI:def_1; ::_thesis: verum end; hence C is directed by WAYBEL_0:def_1; ::_thesis: verum end; registration cluster non empty reflexive transitive antisymmetric locally_directed for RelStr ; existence ex b1 being non empty Poset st b1 is locally_directed proof set R = the non empty discrete Poset; take the non empty discrete Poset ; ::_thesis: the non empty discrete Poset is locally_directed thus the non empty discrete Poset is locally_directed by Th8; ::_thesis: verum end; end; registration cluster non empty non void V73() reflexive transitive antisymmetric order-sorted discernable locally_directed for OverloadedRSSign ; existence ex b1 being OrderSortedSign st b1 is locally_directed proof set R = the discrete OrderSortedSign; take the discrete OrderSortedSign ; ::_thesis: the discrete OrderSortedSign is locally_directed thus the discrete OrderSortedSign is locally_directed by Th8; ::_thesis: verum end; end; registration cluster non empty reflexive transitive antisymmetric discrete -> non empty locally_directed for RelStr ; coherence for b1 being non empty Poset st b1 is discrete holds b1 is locally_directed by Th8; end; registration let S be non empty locally_directed Poset; cluster -> directed for Element of Components S; coherence for b1 being Component of S holds b1 is directed by Def8; end; theorem Th9: :: OSALG_4:9 {} is Equivalence_Relation of {} by RELSET_1:12; 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: :: OSALG_4:def 9 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 ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st for x, y being set holds ( [x,y] in b1 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) proof defpred S1[ 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; percases ( the Sorts of A -carrier_of C is empty or not the Sorts of A -carrier_of C is empty ) ; supposeA2: the Sorts of A -carrier_of C is empty ; ::_thesis: ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st for x, y being set holds ( [x,y] in b1 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) 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 ; ::_thesis: ( [x,y] in {} iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) thus ( [x,y] in {} implies ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) ; ::_thesis: ( ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) implies [x,y] in {} ) assume ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ; ::_thesis: [x,y] in {} 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 [x,y] in {} by A2, TARSKI:def_4; ::_thesis: verum end; hence ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st for x, y being set holds ( [x,y] in b1 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) by A2, Th9; ::_thesis: verum end; suppose not the Sorts of A -carrier_of C is empty ; ::_thesis: ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st for x, y being set holds ( [x,y] in b1 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) 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 : S1[x,y] } ; { [x,y] where x, y is Element of SAC : S1[x,y] } c= [:SAC,SAC:] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { [x,y] where x, y is Element of SAC : S1[x,y] } or z in [:SAC,SAC:] ) assume z in { [x,y] where x, y is Element of SAC : S1[x,y] } ; ::_thesis: z in [:SAC,SAC:] then ex x, y being Element of SAC st ( z = [x,y] & S1[x,y] ) ; hence z in [:SAC,SAC:] by ZFMISC_1:87; ::_thesis: verum end; then reconsider P1 = { [x,y] where x, y is Element of SAC : S1[x,y] } as Relation of SAC ; now__::_thesis:_for_x,_y_being_set_st_x_in_SAC_&_y_in_SAC_&_[x,y]_in_P1_holds_ [y,x]_in_P1 let x, y be set ; ::_thesis: ( x in SAC & y in SAC & [x,y] in P1 implies [y,x] in P1 ) assume that A4: ( x in SAC & y in SAC ) and A5: [x,y] in P1 ; ::_thesis: [y,x] 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: S1[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 { [x,y] where x, y is Element of SAC : S1[x,y] } by A9; hence [y,x] in P1 ; ::_thesis: verum end; then A12: P1 is_symmetric_in SAC by RELAT_2:def_3; now__::_thesis:_for_x_being_set_st_x_in_SAC_holds_ [x,x]_in_P1 let x be set ; ::_thesis: ( x in SAC implies [x,x] in P1 ) assume A13: x in SAC ; ::_thesis: [x,x] in P1 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 { [x,y] where x, y is Element of SAC : S1[x,y] } by A17; hence [x,x] in P1 ; ::_thesis: verum 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__::_thesis:_for_x,_y,_z_being_set_st_x_in_SAC_&_y_in_SAC_&_z_in_SAC_&_[x,y]_in_P1_&_[y,z]_in_P1_holds_ [x,z]_in_P1 let x, y, z be set ; ::_thesis: ( x in SAC & y in SAC & z in SAC & [x,y] in P1 & [y,z] in P1 implies [x,z] in P1 ) assume that x in SAC and y in SAC and z in SAC and A19: [x,y] in P1 and A20: [y,z] in P1 ; ::_thesis: [x,z] in P1 consider x2, y2 being Element of SAC such that A21: [x,y] = [x2,y2] and A22: S1[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: S1[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; ::_thesis: verum end; then P1 is_transitive_in SAC by RELAT_2:def_8; then reconsider P1 = P1 as Equivalence_Relation of ( the Sorts of A -carrier_of C) by A18, A12, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; take P1 ; ::_thesis: for x, y being set holds ( [x,y] in P1 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) for x, y being set holds ( [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } iff S1[x,y] ) proof let x, y be set ; ::_thesis: ( [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } iff S1[x,y] ) hereby ::_thesis: ( S1[x,y] implies [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } ) assume [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } ; ::_thesis: S1[x,y] then ex x1, y1 being Element of SAC st ( [x,y] = [x1,y1] & S1[x1,y1] ) ; hence S1[x,y] ; ::_thesis: verum end; assume A40: S1[x,y] ; ::_thesis: [x,y] in { [x,y] where x, y is Element of SAC : S1[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 { [x,y] where x, y is Element of SAC : S1[x,y] } by A40; hence [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } ; ::_thesis: verum end; hence for x, y being set holds ( [x,y] in P1 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st ( for x, y being set holds ( [x,y] in b1 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being set holds ( [x,y] in b2 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) ) holds b1 = b2 proof let X, Y be Equivalence_Relation of ( the Sorts of A -carrier_of C); ::_thesis: ( ( for x, y being set holds ( [x,y] in X iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being set holds ( [x,y] in Y iff ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) ) implies X = Y ) defpred S1[ 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 S1[x,y] ) ; ::_thesis: ( ex x, y being set st ( ( [x,y] in Y implies ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) ) implies ( ex s1 being Element of S st ( s1 in C & [x,y] in E . s1 ) & not [x,y] in Y ) ) or X = Y ) assume A45: for x, y being set holds ( [x,y] in Y iff S1[x,y] ) ; ::_thesis: X = Y for x, y being set holds ( [x,y] in X iff [x,y] in Y ) proof let x, y be set ; ::_thesis: ( [x,y] in X iff [x,y] in Y ) hereby ::_thesis: ( [x,y] in Y implies [x,y] in X ) assume [x,y] in X ; ::_thesis: [x,y] in Y then S1[x,y] by A44; hence [x,y] in Y by A45; ::_thesis: verum end; assume [x,y] in Y ; ::_thesis: [x,y] in X then S1[x,y] by A45; hence [x,y] in X by A44; ::_thesis: verum end; hence X = Y by RELAT_1:def_2; ::_thesis: verum end; end; :: deftheorem Def9 defines CompClass OSALG_4:def_9_:_ for S being locally_directed OrderSortedSign for A being OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of A for C being Component of S for b5 being Equivalence_Relation of ( the Sorts of A -carrier_of C) holds ( b5 = CompClass (E,C) iff for x, y being set holds ( [x,y] in b5 iff ex s1 being Element of S st ( s1 in C & [x,y] in E . 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: :: OSALG_4:def 10 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 ex b1 being Subset of (Class (CompClass (E,(CComp s1)))) st for z being set holds ( z in b1 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) proof set SAC = the Sorts of A -carrier_of (CComp s1); set CS = Class (CompClass (E,(CComp s1))); defpred S1[ set ] means ex x being set st ( x in the Sorts of A . s1 & \$1 = Class ((CompClass (E,(CComp s1))),x) ); percases ( Class (CompClass (E,(CComp s1))) is empty or not Class (CompClass (E,(CComp s1))) is empty ) ; supposeA1: Class (CompClass (E,(CComp s1))) is empty ; ::_thesis: ex b1 being Subset of (Class (CompClass (E,(CComp s1)))) st for z being set holds ( z in b1 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) reconsider CS1 = {} as Subset of (Class (CompClass (E,(CComp s1)))) by XBOOLE_1:2; take CS1 ; ::_thesis: for z being set holds ( z in CS1 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) let z be set ; ::_thesis: ( z in CS1 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) thus ( z in CS1 implies S1[z] ) ; ::_thesis: ( ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) implies z in CS1 ) assume S1[z] ; ::_thesis: z in CS1 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 the Sorts of A -carrier_of (CComp s1) by A2, Th5; hence z in CS1 by A1; ::_thesis: verum end; suppose not Class (CompClass (E,(CComp s1))) is empty ; ::_thesis: ex b1 being Subset of (Class (CompClass (E,(CComp s1)))) st for z being set holds ( z in b1 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) then reconsider CS1 = Class (CompClass (E,(CComp s1))) as non empty Subset-Family of ( the Sorts of A -carrier_of (CComp s1)) ; set CC = { x where x is Element of CS1 : S1[x] } ; now__::_thesis:_for_x_being_set_st_x_in__{__x_where_x_is_Element_of_CS1_:_S1[x]__}__holds_ x_in_CS1 let x be set ; ::_thesis: ( x in { x where x is Element of CS1 : S1[x] } implies x in CS1 ) assume x in { x where x is Element of CS1 : S1[x] } ; ::_thesis: x in CS1 then ex y being Element of CS1 st ( x = y & S1[y] ) ; hence x in CS1 ; ::_thesis: verum end; then reconsider CC2 = { x where x is Element of CS1 : S1[x] } as Subset of (Class (CompClass (E,(CComp s1)))) by TARSKI:def_3; take CC2 ; ::_thesis: for z being set holds ( z in CC2 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) for x being set holds ( x in { x where x is Element of CS1 : S1[x] } iff S1[x] ) proof let x be set ; ::_thesis: ( x in { x where x is Element of CS1 : S1[x] } iff S1[x] ) hereby ::_thesis: ( S1[x] implies x in { x where x is Element of CS1 : S1[x] } ) assume x in { x where x is Element of CS1 : S1[x] } ; ::_thesis: S1[x] then ex x1 being Element of CS1 st ( x = x1 & S1[x1] ) ; hence S1[x] ; ::_thesis: verum end; assume A3: S1[x] ; ::_thesis: x in { x where x is Element of CS1 : S1[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 x in { x where x is Element of CS1 : S1[x] } by A3; ::_thesis: verum end; hence for z being set holds ( z in CC2 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Subset of (Class (CompClass (E,(CComp s1)))) st ( for z being set holds ( z in b1 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) & ( for z being set holds ( z in b2 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) holds b1 = b2 proof let X, Y be Subset of (Class (CompClass (E,(CComp s1)))); ::_thesis: ( ( for z being set holds ( z in X iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) & ( for z being set holds ( z in Y iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ) implies X = Y ) defpred S1[ 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 S1[x] ) ; ::_thesis: ( ex z being set st ( ( z in Y implies ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) implies ( ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) & not z in Y ) ) or X = Y ) assume A7: for x being set holds ( x in Y iff S1[x] ) ; ::_thesis: X = Y for x being set holds ( x in X iff x in Y ) proof let x be set ; ::_thesis: ( x in X iff x in Y ) hereby ::_thesis: ( x in Y implies x in X ) assume x in X ; ::_thesis: x in Y then S1[x] by A6; hence x in Y by A7; ::_thesis: verum end; assume x in Y ; ::_thesis: x in X then S1[x] by A7; hence x in X by A6; ::_thesis: verum end; hence X = Y by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def10 defines OSClass OSALG_4:def_10_:_ for S being locally_directed OrderSortedSign for A being OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of A for s1 being Element of S for b5 being Subset of (Class (CompClass (E,(CComp s1)))) holds ( b5 = OSClass (E,s1) iff for z being set holds ( z in b5 iff ex x being set st ( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) ); 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 not OSClass (E,s1) is empty 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 not OSClass (E,s1) is empty ; ::_thesis: verum end; end; theorem Th10: :: OSALG_4:10 for S being locally_directed OrderSortedSign for A being OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of A for s1, s2 being Element of S st s1 <= s2 holds OSClass (E,s1) c= OSClass (E,s2) proof let S be locally_directed OrderSortedSign; ::_thesis: for A being OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of A for s1, s2 being Element of S st s1 <= s2 holds OSClass (E,s1) c= OSClass (E,s2) let A be OSAlgebra of S; ::_thesis: for E being MSEquivalence-like OrderSortedRelation of A for s1, s2 being Element of S st s1 <= s2 holds OSClass (E,s1) c= OSClass (E,s2) let E be MSEquivalence-like OrderSortedRelation of A; ::_thesis: for s1, s2 being Element of S st s1 <= s2 holds OSClass (E,s1) c= OSClass (E,s2) let s1, s2 be Element of S; ::_thesis: ( s1 <= s2 implies OSClass (E,s1) c= OSClass (E,s2) ) reconsider s3 = s1, s4 = s2 as Element of S ; assume A1: s1 <= s2 ; ::_thesis: OSClass (E,s1) c= OSClass (E,s2) then A2: CComp s1 = CComp s2 by Th4; thus OSClass (E,s1) c= OSClass (E,s2) ::_thesis: verum proof reconsider SO = the Sorts of A as OrderSortedSet of S by OSALG_1:17; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in OSClass (E,s1) or z in OSClass (E,s2) ) assume z in OSClass (E,s1) ; ::_thesis: z in OSClass (E,s2) 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 z in OSClass (E,s2) by A2, A3, Def10; ::_thesis: verum end; end; 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: :: OSALG_4:def 11 for s1 being Element of S holds it . s1 = OSClass (E,s1); existence ex b1 being OrderSortedSet of S st for s1 being Element of S holds b1 . s1 = OSClass (E,s1) proof deffunc H1( Element of S) -> Subset of (Class (CompClass (E,(CComp \$1)))) = 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 = H1(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; f1 is order-sorted proof let s1, s2 be Element of S; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or f1 . s1 c= f1 . s2 ) assume A3: s1 <= s2 ; ::_thesis: f1 . s1 c= f1 . s2 ( f1 . s1 = OSClass (E,s1) & f1 . s2 = OSClass (E,s2) ) by A2; hence f1 . s1 c= f1 . s2 by A3, Th10; ::_thesis: verum end; hence ex b1 being OrderSortedSet of S st for s1 being Element of S holds b1 . s1 = OSClass (E,s1) by A2; ::_thesis: verum end; uniqueness for b1, b2 being OrderSortedSet of S st ( for s1 being Element of S holds b1 . s1 = OSClass (E,s1) ) & ( for s1 being Element of S holds b2 . s1 = OSClass (E,s1) ) holds b1 = b2 proof let X, Y be OrderSortedSet of S; ::_thesis: ( ( for s1 being Element of S holds X . s1 = OSClass (E,s1) ) & ( for s1 being Element of S holds Y . s1 = OSClass (E,s1) ) implies X = Y ) assume A4: for s1 being Element of S holds X . s1 = OSClass (E,s1) ; ::_thesis: ( ex s1 being Element of S st not Y . s1 = OSClass (E,s1) or X = Y ) assume A5: for s1 being Element of S holds Y . s1 = OSClass (E,s1) ; ::_thesis: X = Y now__::_thesis:_for_s1_being_set_st_s1_in_the_carrier_of_S_holds_ X_._s1_=_Y_._s1 let s1 be set ; ::_thesis: ( s1 in the carrier of S implies X . s1 = Y . s1 ) assume s1 in the carrier of S ; ::_thesis: X . s1 = Y . s1 then reconsider s2 = s1 as Element of S ; thus X . s1 = OSClass (E,s2) by A4 .= Y . s1 by A5 ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def11 defines OSClass OSALG_4:def_11_:_ for S being locally_directed OrderSortedSign for A being OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of A for b4 being OrderSortedSet of S holds ( b4 = OSClass E iff for s1 being Element of S holds b4 . s1 = OSClass (E,s1) ); 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 -> V17() ; coherence OSClass E is non-empty proof for i being set st i in the carrier of S holds not (OSClass E) . i is empty proof let i be set ; ::_thesis: ( i in the carrier of S implies not (OSClass E) . i is empty ) assume i in the carrier of S ; ::_thesis: not (OSClass E) . i is empty then reconsider s = i as Element of S ; (OSClass E) . s = OSClass (E,s) by Def11; hence not (OSClass E) . i is empty ; ::_thesis: verum end; hence OSClass E is non-empty by PBOOLE:def_13; ::_thesis: verum end; end; 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 :: OSALG_4:def 12 Class ((CompClass (E,(CComp s))),x); correctness coherence Class ((CompClass (E,(CComp s))),x) is Element of OSClass (E,s); by Def10; end; :: deftheorem defines OSClass OSALG_4:def_12_:_ for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of U1 for s being Element of S for x being Element of the Sorts of U1 . s holds OSClass (E,x) = Class ((CompClass (E,(CComp s))),x); theorem :: OSALG_4:11 for R being non empty locally_directed Poset for 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 non empty locally_directed Poset; ::_thesis: for 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 ) let x, y be Element of R; ::_thesis: ( ex z being Element of R st ( z <= x & z <= y ) implies ex u being Element of R st ( x <= u & y <= u ) ) assume ex z being Element of R st ( z <= x & z <= y ) ; ::_thesis: ex u being Element of R st ( x <= u & y <= u ) 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 ex u being Element of R st ( x <= u & y <= u ) ; ::_thesis: verum end; theorem Th12: :: OSALG_4:12 for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of U1 for s being Element of S for x, y being 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; ::_thesis: for U1 being non-empty OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of U1 for s being Element of S for x, y being Element of the Sorts of U1 . s holds ( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s ) let U1 be non-empty OSAlgebra of S; ::_thesis: for E being MSEquivalence-like OrderSortedRelation of U1 for s being Element of S for x, y being Element of the Sorts of U1 . s holds ( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s ) let E be MSEquivalence-like OrderSortedRelation of U1; ::_thesis: for s being Element of S for x, y being Element of the Sorts of U1 . s holds ( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s ) let s be Element of S; ::_thesis: for x, y being Element of the Sorts of U1 . s holds ( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s ) let x, y be Element of the Sorts of U1 . s; ::_thesis: ( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . 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 ::_thesis: ( [x,y] in E . s implies OSClass (E,x) = OSClass (E,y) ) assume OSClass (E,x) = OSClass (E,y) ; ::_thesis: [x,y] in E . s 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; ::_thesis: verum 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 ; ::_thesis: OSClass (E,x) = OSClass (E,y) then [x,y] in CompClass (E,(CComp s)) by A8, Def9; hence OSClass (E,x) = OSClass (E,y) by A9, EQREL_1:35; ::_thesis: verum end; theorem :: OSALG_4:13 for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for E being MSEquivalence-like OrderSortedRelation of U1 for s1, s2 being Element of S for x being 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 definition let S be locally_directed OrderSortedSign; let o be Element of the carrier' of S; let A be non-empty OSAlgebra of S; let R be OSCongruence of A; let x be Element of Args (o,A); funcR #_os x -> Element of product ((OSClass R) * (the_arity_of o)) means :Def13: :: OSALG_4:def 13 for n being 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 & it . n = OSClass (R,y) ); existence ex b1 being Element of product ((OSClass R) * (the_arity_of o)) st for n being 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 & b1 . n = OSClass (R,y) ) proof defpred S1[ set , set ] means for n being 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; set da = dom (the_arity_of o); A1: for k being set st k in dom (the_arity_of o) holds ex u being set st S1[k,u] proof let k be set ; ::_thesis: ( k in dom (the_arity_of o) implies ex u being set st S1[k,u] ) assume A2: k in dom (the_arity_of o) ; ::_thesis: ex u being set st S1[k,u] 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) ; ::_thesis: S1[k, OSClass (R,y)] thus S1[k, OSClass (R,y)] ; ::_thesis: verum end; consider f being Function such that A3: ( dom f = dom (the_arity_of o) & ( for x being set st x in dom (the_arity_of o) holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); A4: dom ((OSClass R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2; for y being set st y in dom ((OSClass R) * (the_arity_of o)) holds f . y in ((OSClass R) * (the_arity_of o)) . y proof let y be set ; ::_thesis: ( y in dom ((OSClass R) * (the_arity_of o)) implies f . y in ((OSClass R) * (the_arity_of o)) . y ) assume A5: y in dom ((OSClass R) * (the_arity_of o)) ; ::_thesis: f . y in ((OSClass R) * (the_arity_of o)) . y then reconsider n = y as Nat ; (the_arity_of o) . y in rng (the_arity_of o) by A4, A5, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . 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) ) & (the_arity_of o) /. n = (the_arity_of o) . n ) by A3, A4, A5, PARTFUN1:def_6; then A6: f . y in OSClass (R,s) ; ((OSClass R) * (the_arity_of o)) . y = (OSClass R) . ((the_arity_of o) . y) by A5, FUNCT_1:12; hence f . y in ((OSClass R) * (the_arity_of o)) . y by A6, Def11; ::_thesis: verum end; then reconsider f = f as Element of product ((OSClass R) * (the_arity_of o)) by A3, A4, CARD_3:9; take f ; ::_thesis: for n being 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) ) let n be Nat; ::_thesis: ( n in dom (the_arity_of o) implies ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st ( y = x . n & f . n = OSClass (R,y) ) ) assume n in dom (the_arity_of o) ; ::_thesis: ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st ( y = x . n & f . n = OSClass (R,y) ) hence ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st ( y = x . n & f . n = OSClass (R,y) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Element of product ((OSClass R) * (the_arity_of o)) st ( for n being 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 & b1 . n = OSClass (R,y) ) ) & ( for n being 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 & b2 . n = OSClass (R,y) ) ) holds b1 = b2 proof let F, G be Element of product ((OSClass R) * (the_arity_of o)); ::_thesis: ( ( for n being 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 being 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) ) ) implies F = G ) assume A7: ( ( for n being 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 being 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) ) ) ) ; ::_thesis: F = G A8: for y being set st y in dom (the_arity_of o) holds F . y = G . y proof let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies F . y = G . y ) assume A9: y in dom (the_arity_of o) ; ::_thesis: F . y = G . y 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 F . y = G . y ; ::_thesis: verum 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 F = G by A10, A8, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def13 defines #_os OSALG_4:def_13_:_ for S being locally_directed OrderSortedSign for o being Element of the carrier' of S for A being non-empty OSAlgebra of S for R being OSCongruence of A for x being Element of Args (o,A) for b6 being Element of product ((OSClass R) * (the_arity_of o)) holds ( b6 = R #_os x iff for n being 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 & b6 . n = OSClass (R,y) ) ); definition let S be locally_directed OrderSortedSign; let o be Element of the carrier' of S; 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: :: OSALG_4:def 14 for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = OSClass (R,x); existence ex b1 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = OSClass (R,x) proof set rs = the_result_sort_of o; set D = the Sorts of A . (the_result_sort_of o); deffunc H1( Element of the Sorts of A . (the_result_sort_of o)) -> Element of OSClass (R,(the_result_sort_of o)) = OSClass (R,\$1); consider f being Function such that A1: ( dom f = the Sorts of A . (the_result_sort_of o) & ( for d being Element of the Sorts of A . (the_result_sort_of o) holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); A2: for x being set st x in the Sorts of A . (the_result_sort_of o) holds f . x in (OSClass R) . (the_result_sort_of o) proof let x be set ; ::_thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x in (OSClass R) . (the_result_sort_of o) ) assume x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: f . x in (OSClass R) . (the_result_sort_of o) then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ; f . x1 = OSClass (R,x1) by A1; then f . x1 in OSClass (R,(the_result_sort_of o)) ; hence f . x in (OSClass R) . (the_result_sort_of o) by Def11; ::_thesis: verum 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 .= the Sorts of A . (the_result_sort_of o) 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) . (the_result_sort_of o) by MSUALG_1:def_2 ; then reconsider f = 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 ; ::_thesis: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) thus for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = OSClass (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = OSClass (R,x) ) holds b1 = b2 proof set SA = the Sorts of A; set RS = the ResultSort of S; set 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); ::_thesis: ( ( for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = OSClass (R,x) ) implies f = g ) assume that A5: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass (R,x) and A6: for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = OSClass (R,x) ; ::_thesis: f = g A7: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_A_._(the_result_sort_of_o)_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x = g . x ) assume x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: f . x = g . x then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ; f . x1 = OSClass (R,x1) by A5; hence f . x = g . x by A6; ::_thesis: verum end; o in the carrier' of S ; then o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def_2; then ( 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 . (the_result_sort_of o) by MSUALG_1:def_2 ; then ( dom f = the Sorts of A . (the_result_sort_of o) & dom g = the Sorts of A . (the_result_sort_of o) ) by FUNCT_2:def_1; hence f = g by A7, FUNCT_1:2; ::_thesis: verum end; func OSQuotArgs (R,o) -> Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) means :: OSALG_4:def 15 for x being Element of Args (o,A) holds it . x = R #_os x; existence ex b1 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st for x being Element of Args (o,A) holds b1 . x = R #_os x proof set ao = the_arity_of o; set D = Args (o,A); deffunc H1( Element of Args (o,A)) -> Element of product ((OSClass R) * (the_arity_of o)) = R #_os \$1; consider f being Function such that A8: ( dom f = Args (o,A) & ( for d being Element of Args (o,A) holds f . d = H1(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 being set st x in ( the Sorts of A #) . (the_arity_of o) holds f . x in ((OSClass R) #) . (the_arity_of o) proof let x be set ; ::_thesis: ( x in ( the Sorts of A #) . (the_arity_of o) implies f . x in ((OSClass R) #) . (the_arity_of o) ) assume x in ( the Sorts of A #) . (the_arity_of o) ; ::_thesis: f . x in ((OSClass R) #) . (the_arity_of o) then reconsider x1 = x as Element of Args (o,A) by A10, MSUALG_1:def_4; ( f . x1 = R #_os x1 & ((OSClass R) #) . (the_arity_of o) = product ((OSClass R) * (the_arity_of o)) ) by A8, FINSEQ_2:def_5; hence f . x in ((OSClass R) #) . (the_arity_of o) ; ::_thesis: verum 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) #) . (the_arity_of o) by MSUALG_1:def_1 ; then reconsider f = 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 ; ::_thesis: for x being Element of Args (o,A) holds f . x = R #_os x thus for x being Element of Args (o,A) holds f . x = R #_os x by A8; ::_thesis: verum end; uniqueness for b1, b2 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b1 . x = R #_os x ) & ( for x being Element of Args (o,A) holds b2 . x = R #_os x ) holds b1 = b2 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); ::_thesis: ( ( for x being Element of Args (o,A) holds f . x = R #_os x ) & ( for x being Element of Args (o,A) holds g . x = R #_os x ) implies f = g ) assume that A12: for x being Element of Args (o,A) holds f . x = R #_os x and A13: for x being Element of Args (o,A) holds g . x = R #_os x ; ::_thesis: f = g 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__::_thesis:_for_x_being_set_st_x_in_(_the_Sorts_of_A_#)_._(the_arity_of_o)_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in ( the Sorts of A #) . (the_arity_of o) implies f . x = g . x ) assume x in ( the Sorts of A #) . (the_arity_of o) ; ::_thesis: f . x = g . x 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; ::_thesis: verum end; ( dom f = ( the Sorts of A #) . (the_arity_of o) & dom g = ( the Sorts of A #) . (the_arity_of o) ) by A14, FUNCT_2:def_1; hence f = g by A15, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def14 defines OSQuotRes OSALG_4:def_14_:_ for S being locally_directed OrderSortedSign for o being Element of the carrier' of S for A being non-empty OSAlgebra of S for R being OSCongruence of A for b5 being Function of (( the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) holds ( b5 = OSQuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = OSClass (R,x) ); :: deftheorem defines OSQuotArgs OSALG_4:def_15_:_ for S being locally_directed OrderSortedSign for o being Element of the carrier' of S for A being non-empty OSAlgebra of S for R being OSCongruence of A for b5 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o) holds ( b5 = OSQuotArgs (R,o) iff for x being Element of Args (o,A) holds b5 . x = R #_os x ); definition let S be locally_directed OrderSortedSign; 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 :: OSALG_4:def 16 for o being OperSymbol of S holds it . o = OSQuotRes (R,o); existence ex b1 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st for o being OperSymbol of S holds b1 . o = OSQuotRes (R,o) proof defpred S1[ set , set ] means for o being OperSymbol of S st o = \$1 holds \$2 = OSQuotRes (R,o); set O = the carrier' of S; A1: for x being set st x in the carrier' of S holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] ) assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y] then reconsider x1 = x as OperSymbol of S ; take OSQuotRes (R,x1) ; ::_thesis: S1[x, OSQuotRes (R,x1)] thus S1[x, OSQuotRes (R,x1)] ; ::_thesis: verum end; consider f being Function such that A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider x1 = x as OperSymbol of S ; f . x1 = OSQuotRes (R,x1) by A2; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6; for i being set st i in the carrier' of S 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 ; ::_thesis: ( i in the carrier' of S implies f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((OSClass R) * the ResultSort of S) . i) ) assume i in the carrier' of S ; ::_thesis: f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((OSClass R) * the ResultSort of S) . i) then reconsider i1 = i as OperSymbol of S ; f . i1 = OSQuotRes (R,i1) by A2; hence f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((OSClass R) * the ResultSort of S) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S by PBOOLE:def_15; take f ; ::_thesis: for o being OperSymbol of S holds f . o = OSQuotRes (R,o) thus for o being OperSymbol of S holds f . o = OSQuotRes (R,o) by A2; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = OSQuotRes (R,o) ) & ( for o being OperSymbol of S holds b2 . o = OSQuotRes (R,o) ) holds b1 = b2 proof let f, g be ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = OSQuotRes (R,o) ) & ( for o being OperSymbol of S holds g . o = OSQuotRes (R,o) ) implies f = g ) 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) ; ::_thesis: f = g now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_ f_._i_=_g_._i let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i ) assume i in the carrier' of S ; ::_thesis: f . i = g . i then reconsider i1 = i as OperSymbol of S ; f . i1 = OSQuotRes (R,i1) by A3; hence f . i = g . i by A4; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; func OSQuotArgs R -> ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S means :: OSALG_4:def 17 for o being OperSymbol of S holds it . o = OSQuotArgs (R,o); existence ex b1 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st for o being OperSymbol of S holds b1 . o = OSQuotArgs (R,o) proof defpred S1[ set , set ] means for o being OperSymbol of S st o = \$1 holds \$2 = OSQuotArgs (R,o); set O = the carrier' of S; A5: for x being set st x in the carrier' of S holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] ) assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y] then reconsider x1 = x as OperSymbol of S ; take OSQuotArgs (R,x1) ; ::_thesis: S1[x, OSQuotArgs (R,x1)] thus S1[x, OSQuotArgs (R,x1)] ; ::_thesis: verum end; consider f being Function such that A6: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds S1[x,f . x] ) ) from CLASSES1:sch_1(A5); reconsider f = f as ManySortedSet of the carrier' of S by A6, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider x1 = x as OperSymbol of S ; f . x1 = OSQuotArgs (R,x1) by A6; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6; for i being set st i in the carrier' of S 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 ; ::_thesis: ( i in the carrier' of S implies f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i) ) assume i in the carrier' of S ; ::_thesis: f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i) then reconsider i1 = i as OperSymbol of S ; f . i1 = OSQuotArgs (R,i1) by A6; hence f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((OSClass R) #) * the Arity of S) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S by PBOOLE:def_15; take f ; ::_thesis: for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) thus for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) by A6; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S st ( for o being OperSymbol of S holds b1 . o = OSQuotArgs (R,o) ) & ( for o being OperSymbol of S holds b2 . o = OSQuotArgs (R,o) ) holds b1 = b2 proof let f, g be ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = OSQuotArgs (R,o) ) & ( for o being OperSymbol of S holds g . o = OSQuotArgs (R,o) ) implies f = g ) 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) ; ::_thesis: f = g now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_ f_._i_=_g_._i let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i ) assume i in the carrier' of S ; ::_thesis: f . i = g . i then reconsider i1 = i as OperSymbol of S ; f . i1 = OSQuotArgs (R,i1) by A7; hence f . i = g . i by A8; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem defines OSQuotRes OSALG_4:def_16_:_ for S being locally_directed OrderSortedSign for A being non-empty OSAlgebra of S for R being OSCongruence of A for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(OSClass R) * the ResultSort of S holds ( b4 = OSQuotRes R iff for o being OperSymbol of S holds b4 . o = OSQuotRes (R,o) ); :: deftheorem defines OSQuotArgs OSALG_4:def_17_:_ for S being locally_directed OrderSortedSign for A being non-empty OSAlgebra of S for R being OSCongruence of A for b4 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((OSClass R) #) * the Arity of S holds ( b4 = OSQuotArgs R iff for o being OperSymbol of S holds b4 . o = OSQuotArgs (R,o) ); theorem Th14: :: OSALG_4:14 for S being locally_directed OrderSortedSign for o being Element of the carrier' of S for A being non-empty OSAlgebra of S for R being OSCongruence of A for x being set st x in (((OSClass R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R #_os a proof let S be locally_directed OrderSortedSign; ::_thesis: for o being Element of the carrier' of S for A being non-empty OSAlgebra of S for R being OSCongruence of A for x being set st x in (((OSClass R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R #_os a let o be Element of the carrier' of S; ::_thesis: for A being non-empty OSAlgebra of S for R being OSCongruence of A for x being set st x in (((OSClass R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R #_os a let A be non-empty OSAlgebra of S; ::_thesis: for R being OSCongruence of A for x being set st x in (((OSClass R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R #_os a let R be OSCongruence of A; ::_thesis: for x being set st x in (((OSClass R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R #_os a let x be set ; ::_thesis: ( x in (((OSClass R) #) * the Arity of S) . o implies ex a being Element of Args (o,A) st x = R #_os a ) assume A1: x in (((OSClass R) #) * the Arity of S) . o ; ::_thesis: ex a being Element of Args (o,A) st x = R #_os a set ar = the_arity_of o; A2: the_arity_of o = the Arity of S . o by MSUALG_1:def_1; then (((OSClass R) #) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o)) by MSAFREE:1; then consider f being Function such that A3: f = x and A4: dom f = dom ((OSClass R) * (the_arity_of o)) and A5: for y being set st y in dom ((OSClass R) * (the_arity_of o)) holds f . y in ((OSClass R) * (the_arity_of o)) . y by A1, CARD_3:def_5; defpred S1[ set , set ] means ( \$2 in the Sorts of A . ((the_arity_of o) /. \$1) & \$2 in f . \$1 ); A6: dom ((OSClass R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2; A7: for n being Nat st n in dom f holds f . n in OSClass (R,((the_arity_of o) /. n)) proof let n be Nat; ::_thesis: ( n in dom f implies f . n in OSClass (R,((the_arity_of o) /. n)) ) reconsider s = (the_arity_of o) /. n as Element of S ; assume A8: n in dom f ; ::_thesis: f . n in OSClass (R,((the_arity_of o) /. n)) then (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, PARTFUN1:def_6; then ((OSClass R) * (the_arity_of o)) . n = (OSClass R) . s by A4, A8, FUNCT_1:12 .= OSClass (R,s) by Def11 ; hence f . n in OSClass (R,((the_arity_of o) /. n)) by A4, A5, A8; ::_thesis: verum end; A9: for a being set st a in dom f holds ex b being set st S1[a,b] proof let a be set ; ::_thesis: ( a in dom f implies ex b being set st S1[a,b] ) reconsider s = (the_arity_of o) /. a as Element of S ; assume A10: a in dom f ; ::_thesis: ex b being set st S1[a,b] 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 ; ::_thesis: S1[a,x] thus S1[a,x] by A11, Th5, EQREL_1:20; ::_thesis: verum end; consider g being Function such that A12: ( dom g = dom f & ( for a being set st a in dom f holds S1[a,g . a] ) ) from CLASSES1:sch_1(A9); dom the Sorts of A = the carrier of S by PARTFUN1:def_2; then rng (the_arity_of o) c= dom the Sorts of A ; then A13: dom g = dom ( the Sorts of A * (the_arity_of o)) by A4, A6, A12, RELAT_1:27; A14: for y being set st y in dom ( the Sorts of A * (the_arity_of o)) holds g . y in ( the Sorts of A * (the_arity_of o)) . y proof let y be set ; ::_thesis: ( y in dom ( the Sorts of A * (the_arity_of o)) implies g . y in ( the Sorts of A * (the_arity_of o)) . y ) assume A15: y in dom ( the Sorts of A * (the_arity_of o)) ; ::_thesis: g . y in ( the Sorts of A * (the_arity_of o)) . y then reconsider n = y as Nat ; reconsider s = (the_arity_of o) /. n as Element of S ; ( (the_arity_of o) . n = (the_arity_of o) /. n & g . n in the Sorts of A . s ) by A4, A6, A12, A13, A15, PARTFUN1:def_6; hence g . y in ( the Sorts of A * (the_arity_of o)) . y by A15, FUNCT_1:12; ::_thesis: verum end; Args (o,A) = (( the Sorts of A #) * the Arity of S) . o by MSUALG_1:def_4 .= product ( the Sorts of A * (the_arity_of o)) by A2, MSAFREE:1 ; then reconsider g = g as Element of Args (o,A) by A13, A14, CARD_3:9; A16: for x being set st x in dom (the_arity_of o) holds f . x = (R #_os g) . x proof let x be set ; ::_thesis: ( x in dom (the_arity_of o) implies f . x = (R #_os g) . x ) assume A17: x in dom (the_arity_of o) ; ::_thesis: f . x = (R #_os g) . x 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 = (the_arity_of o) /. 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 f . x = (R #_os g) . x by A18, A20, EQREL_1:23; ::_thesis: verum end; take g ; ::_thesis: x = R #_os g dom (R #_os g) = dom ((OSClass R) * (the_arity_of o)) by CARD_3:9; hence x = R #_os g by A3, A4, A6, A16, FUNCT_1:2; ::_thesis: verum end; definition let S be locally_directed OrderSortedSign; let o be Element of the carrier' of S; 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: :: OSALG_4:def 18 for a being 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 ex b1 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds b1 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a proof defpred S1[ set , set ] means for a being 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; set Cr = ((OSClass R) * the ResultSort of S) . o; A1: for x being set st x in (((OSClass R) #) * the Arity of S) . o holds ex y being set st ( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] ) proof set ro = the_result_sort_of o; set ar = the_arity_of o; let x be set ; ::_thesis: ( x in (((OSClass R) #) * the Arity of S) . o implies ex y being set st ( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] ) ) assume x in (((OSClass R) #) * the Arity of S) . o ; ::_thesis: ex y being set st ( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] ) then consider a being Element of Args (o,A) such that A2: x = R #_os a by Th14; take y = ((OSQuotRes (R,o)) * (Den (o,A))) . a; ::_thesis: ( y in ((OSClass R) * the ResultSort of S) . o & S1[x,y] ) 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) . (the_result_sort_of o) 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 . (the_result_sort_of o) by MSUALG_1:def_2 ; then A6: ( dom (OSQuotRes (R,o)) = the Sorts of A . (the_result_sort_of o) & Result (o,A) = the Sorts of A . (the_result_sort_of o) ) 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) . (the_result_sort_of o) by A4; hence y in ((OSClass R) * the ResultSort of S) . o by A4, A7, FUNCT_1:12; ::_thesis: S1[x,y] let b be Element of Args (o,A); ::_thesis: ( x = R #_os b implies y = ((OSQuotRes (R,o)) * (Den (o,A))) . b ) reconsider da = (Den (o,A)) . a, db = (Den (o,A)) . b as Element of the Sorts of A . (the_result_sort_of o) 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 (the_result_sort_of o)))),db) ; assume A9: x = R #_os b ; ::_thesis: y = ((OSQuotRes (R,o)) * (Den (o,A))) . b for n being Nat st n in dom a holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) proof let n be Nat; ::_thesis: ( n in dom a implies [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) A10: dom a = dom (the_arity_of o) by MSUALG_3:6; assume n in dom a ; ::_thesis: [(a . n),(b . n)] in R . ((the_arity_of o) /. n) then ( ex ya being Element of the Sorts of A . ((the_arity_of o) /. n) st ( ya = a . n & (R #_os a) . n = OSClass (R,ya) ) & ex yb being Element of the Sorts of A . ((the_arity_of o) /. n) st ( yb = b . n & (R #_os b) . n = OSClass (R,yb) ) ) by A10, Def13; hence [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, Th12; ::_thesis: verum end; then ( the_result_sort_of o in CComp (the_result_sort_of o) & [da,db] in R . (the_result_sort_of o) ) by EQREL_1:20, MSUALG_4:def_4; then A11: [da,db] in CompClass (R,(CComp (the_result_sort_of o))) by Def9; A12: da in the Sorts of A -carrier_of (CComp (the_result_sort_of o)) by Th5; y = (OSQuotRes (R,o)) . ((Den (o,A)) . a) by A7, FUNCT_1:12 .= OSClass (R,da) by Def14 .= Class ((CompClass (R,(CComp (the_result_sort_of o)))),da) ; hence y = ((OSQuotRes (R,o)) * (Den (o,A))) . b by A12, A8, A11, EQREL_1:35; ::_thesis: verum end; consider f being Function such that A13: ( dom f = (((OSClass R) #) * the Arity of S) . o & rng f c= ((OSClass R) * the ResultSort of S) . o & ( for x being set st x in (((OSClass R) #) * the Arity of S) . o holds S1[x,f . x] ) ) from FUNCT_1:sch_5(A1); reconsider f = 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 ; ::_thesis: for a being 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 thus for a being 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 by A13; ::_thesis: verum end; uniqueness for b1, b2 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds b1 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds b2 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ) holds b1 = b2 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); ::_thesis: ( ( for a being 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 ) & ( for a being 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 ) implies F = G ) assume that A14: for a being 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 being 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 ; ::_thesis: F = G 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) #) . (the_arity_of o) by MSUALG_1:def_1 ; A18: now__::_thesis:_for_x_being_set_st_x_in_((OSClass_R)_#)_._(the_arity_of_o)_holds_ F_._x_=_G_._x let x be set ; ::_thesis: ( x in ((OSClass R) #) . (the_arity_of o) implies F . x = G . x ) assume A19: x in ((OSClass R) #) . (the_arity_of o) ; ::_thesis: F . x = G . x then consider a being 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; ::_thesis: verum end; ( dom F = ((OSClass R) #) . (the_arity_of o) & dom G = ((OSClass R) #) . (the_arity_of o) ) by A17, FUNCT_2:def_1; hence F = G by A18, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def18 defines OSQuotCharact OSALG_4:def_18_:_ for S being locally_directed OrderSortedSign for o being Element of the carrier' of S for A being non-empty OSAlgebra of S for R being OSCongruence of A for b5 being Function of ((((OSClass R) #) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o) holds ( b5 = OSQuotCharact (R,o) iff for a being Element of Args (o,A) st R #_os a in (((OSClass R) #) * the Arity of S) . o holds b5 . (R #_os a) = ((OSQuotRes (R,o)) * (Den (o,A))) . a ); definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 19 for o being OperSymbol of S holds it . o = OSQuotCharact (R,o); existence ex b1 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st for o being OperSymbol of S holds b1 . o = OSQuotCharact (R,o) proof defpred S1[ set , set ] means for o being OperSymbol of S st o = \$1 holds \$2 = OSQuotCharact (R,o); set O = the carrier' of S; A1: for x being set st x in the carrier' of S holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] ) assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y] then reconsider x1 = x as OperSymbol of S ; take OSQuotCharact (R,x1) ; ::_thesis: S1[x, OSQuotCharact (R,x1)] thus S1[x, OSQuotCharact (R,x1)] ; ::_thesis: verum end; consider f being Function such that A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider x1 = x as OperSymbol of S ; f . x1 = OSQuotCharact (R,x1) by A2; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6; for i being set st i in the carrier' of S 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 ; ::_thesis: ( i in the carrier' of S implies f . i is Function of ((((OSClass R) #) * the Arity of S) . i),(((OSClass R) * the ResultSort of S) . i) ) assume i in the carrier' of S ; ::_thesis: f . i is Function of ((((OSClass R) #) * the Arity of S) . i),(((OSClass R) * the ResultSort of S) . i) then reconsider i1 = i as OperSymbol of S ; f . i1 = OSQuotCharact (R,i1) by A2; hence f . i is Function of ((((OSClass R) #) * the Arity of S) . i),(((OSClass R) * the ResultSort of S) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S by PBOOLE:def_15; take f ; ::_thesis: for o being OperSymbol of S holds f . o = OSQuotCharact (R,o) thus for o being OperSymbol of S holds f . o = OSQuotCharact (R,o) by A2; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = OSQuotCharact (R,o) ) & ( for o being OperSymbol of S holds b2 . o = OSQuotCharact (R,o) ) holds b1 = b2 proof let f, g be ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = OSQuotCharact (R,o) ) & ( for o being OperSymbol of S holds g . o = OSQuotCharact (R,o) ) implies f = g ) 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) ; ::_thesis: f = g now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_ f_._i_=_g_._i let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i ) assume i in the carrier' of S ; ::_thesis: f . i = g . i then reconsider i1 = i as OperSymbol of S ; f . i1 = OSQuotCharact (R,i1) by A3; hence f . i = g . i by A4; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def19 defines OSQuotCharact OSALG_4:def_19_:_ for S being locally_directed OrderSortedSign for A being non-empty OSAlgebra of S for R being OSCongruence of A for b4 being ManySortedFunction of ((OSClass R) #) * the Arity of S,(OSClass R) * the ResultSort of S holds ( b4 = OSQuotCharact R iff for o being OperSymbol of S holds b4 . o = OSQuotCharact (R,o) ); definition let S be locally_directed OrderSortedSign; let U1 be non-empty OSAlgebra of S; let R be OSCongruence of U1; func QuotOSAlg (U1,R) -> OSAlgebra of S equals :: OSALG_4:def 20 MSAlgebra(# (OSClass R),(OSQuotCharact R) #); coherence MSAlgebra(# (OSClass R),(OSQuotCharact R) #) is OSAlgebra of S by OSALG_1:17; end; :: deftheorem defines QuotOSAlg OSALG_4:def_20_:_ for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for R being OSCongruence of U1 holds QuotOSAlg (U1,R) = MSAlgebra(# (OSClass R),(OSQuotCharact R) #); registration let S be locally_directed OrderSortedSign; let U1 be non-empty OSAlgebra of S; let R be OSCongruence of U1; cluster QuotOSAlg (U1,R) -> strict non-empty ; coherence ( QuotOSAlg (U1,R) is strict & QuotOSAlg (U1,R) is non-empty ) by MSUALG_1:def_3; end; definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 21 for x being Element of the Sorts of U1 . s holds it . x = OSClass (R,x); existence ex b1 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st for x being Element of the Sorts of U1 . s holds b1 . x = OSClass (R,x) proof deffunc H1( Element of the Sorts of U1 . s) -> Element of OSClass (R,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 = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) st ( for x being Element of the Sorts of U1 . s holds b1 . x = OSClass (R,x) ) & ( for x being Element of the Sorts of U1 . s holds b2 . x = OSClass (R,x) ) holds b1 = b2 proof let f, g be Function of ( the Sorts of U1 . s),(OSClass (R,s)); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds f . x = OSClass (R,x) ) & ( for x being Element of the Sorts of U1 . s holds g . x = OSClass (R,x) ) implies f = g ) 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) ; ::_thesis: f = g A3: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_U1_._s_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in the Sorts of U1 . s implies f . x = g . x ) assume x in the Sorts of U1 . s ; ::_thesis: f . x = g . x 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; ::_thesis: verum end; ( dom f = the Sorts of U1 . s & dom g = the Sorts of U1 . s ) by FUNCT_2:def_1; hence f = g by A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def21 defines OSNat_Hom OSALG_4:def_21_:_ for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for R being OSCongruence of U1 for s being Element of S for b5 being Function of ( the Sorts of U1 . s),(OSClass (R,s)) holds ( b5 = OSNat_Hom (U1,R,s) iff for x being Element of the Sorts of U1 . s holds b5 . x = OSClass (R,x) ); definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 22 for s being Element of S holds it . s = OSNat_Hom (U1,R,s); existence ex b1 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st for s being Element of S holds b1 . s = OSNat_Hom (U1,R,s) proof deffunc H1( Element of S) -> Function of ( the Sorts of U1 . \$1),(OSClass (R,\$1)) = OSNat_Hom (U1,R,\$1); consider f being Function such that A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider y = x as Element of S ; f . y = OSNat_Hom (U1,R,y) by A1; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6; for i being 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 ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of U1 . i),((OSClass R) . i) ) assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of U1 . i),((OSClass R) . i) 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 f . i is Function of ( the Sorts of U1 . i),((OSClass R) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Sorts of U1, OSClass R by PBOOLE:def_15; reconsider f = f as ManySortedFunction of U1,(QuotOSAlg (U1,R)) ; take f ; ::_thesis: for s being Element of S holds f . s = OSNat_Hom (U1,R,s) thus for s being Element of S holds f . s = OSNat_Hom (U1,R,s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) st ( for s being Element of S holds b1 . s = OSNat_Hom (U1,R,s) ) & ( for s being Element of S holds b2 . s = OSNat_Hom (U1,R,s) ) holds b1 = b2 proof let F, G be ManySortedFunction of U1,(QuotOSAlg (U1,R)); ::_thesis: ( ( for s being Element of S holds F . s = OSNat_Hom (U1,R,s) ) & ( for s being Element of S holds G . s = OSNat_Hom (U1,R,s) ) implies F = G ) assume that A2: for s being Element of S holds F . s = OSNat_Hom (U1,R,s) and A3: for s being Element of S holds G . s = OSNat_Hom (U1,R,s) ; ::_thesis: F = G now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ F_._i_=_G_._i let i be set ; ::_thesis: ( i in the carrier of S implies F . i = G . i ) assume i in the carrier of S ; ::_thesis: F . i = G . i then reconsider s = i as SortSymbol of S ; F . s = OSNat_Hom (U1,R,s) by A2; hence F . i = G . i by A3; ::_thesis: verum end; hence F = G by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def22 defines OSNat_Hom OSALG_4:def_22_:_ for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for R being OSCongruence of U1 for b4 being ManySortedFunction of U1,(QuotOSAlg (U1,R)) holds ( b4 = OSNat_Hom (U1,R) iff for s being Element of S holds b4 . s = OSNat_Hom (U1,R,s) ); theorem :: OSALG_4:15 for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for R being OSCongruence of U1 holds ( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted ) proof let S be locally_directed OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S for R being OSCongruence of U1 holds ( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted ) let U1 be non-empty OSAlgebra of S; ::_thesis: for R being OSCongruence of U1 holds ( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted ) let R be OSCongruence of U1; ::_thesis: ( OSNat_Hom (U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom (U1,R) is order-sorted ) set F = OSNat_Hom (U1,R); set QA = QuotOSAlg (U1,R); set S1 = the Sorts of U1; for o being Element of the carrier' of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) proof let o be Element of the carrier' of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) ) assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) let x be Element of Args (o,U1); ::_thesis: ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) set ro = the_result_sort_of o; set ar = the_arity_of o; the Arity of S . o = the_arity_of o by MSUALG_1:def_1; then A1: (((OSClass R) #) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o)) by MSAFREE:1; A2: dom x = dom (the_arity_of o) by MSUALG_3:6; A3: for a being set st a in dom (the_arity_of o) holds ((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a proof let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies ((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a ) assume A4: a in dom (the_arity_of o) ; ::_thesis: ((OSNat_Hom (U1,R)) # x) . a = (R #_os x) . a then reconsider n = a as Nat ; set Fo = OSNat_Hom (U1,R,((the_arity_of o) /. n)); set s = (the_arity_of o) /. n; A5: ex z being Element of the Sorts of U1 . ((the_arity_of o) /. n) st ( z = x . n & (R #_os x) . n = OSClass (R,z) ) by A4, Def13; A6: n in dom ( the Sorts of U1 * (the_arity_of o)) by A4, PARTFUN1:def_2; then ( the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) . n) by FUNCT_1:12 .= the Sorts of U1 . ((the_arity_of o) /. n) by A4, PARTFUN1:def_6 ; then reconsider xn = x . n as Element of the Sorts of U1 . ((the_arity_of o) /. n) by A6, MSUALG_3:6; thus ((OSNat_Hom (U1,R)) # x) . a = ((OSNat_Hom (U1,R)) . ((the_arity_of o) /. n)) . (x . n) by A2, A4, MSUALG_3:def_6 .= (OSNat_Hom (U1,R,((the_arity_of o) /. n))) . xn by Def22 .= (R #_os x) . a by A5, Def21 ; ::_thesis: verum 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 . (the_result_sort_of o) by MSUALG_1:def_2 ; then reconsider dx = (Den (o,U1)) . x as Element of the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_5; ( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) 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 (the_arity_of o) c= dom (OSClass R) ) by CARD_3:9; then ( dom ((OSNat_Hom (U1,R)) # x) = dom (the_arity_of o) & dom (R #_os x) = dom (the_arity_of o) ) by MSUALG_3:6, RELAT_1:27; then A9: (OSNat_Hom (U1,R)) # x = R #_os x by A3, FUNCT_1:2; Den (o,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o by MSUALG_1:def_6 .= OSQuotCharact (R,o) by Def19 ; then (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # 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,(the_result_sort_of o))) . dx by Def21 .= ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) by Def22 ; hence ((OSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotOSAlg (U1,R)))) . ((OSNat_Hom (U1,R)) # x) ; ::_thesis: verum end; hence OSNat_Hom (U1,R) is_homomorphism U1, QuotOSAlg (U1,R) by MSUALG_3:def_7; :: according to MSUALG_3:def_8 ::_thesis: ( OSNat_Hom (U1,R) is "onto" & OSNat_Hom (U1,R) is order-sorted ) for i being set st i in the carrier of S holds rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i ) assume i in the carrier of S ; ::_thesis: rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i then reconsider s = i as Element of S ; reconsider f = (OSNat_Hom (U1,R)) . i as Function of ( the Sorts of U1 . s),( the Sorts of (QuotOSAlg (U1,R)) . s) by PBOOLE:def_15; A10: dom f = the Sorts of U1 . s by FUNCT_2:def_1; A11: the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s) by Def11; for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . i holds x in rng f proof let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,R)) . i implies x in rng f ) A12: f = OSNat_Hom (U1,R,s) by Def22; assume x in the Sorts of (QuotOSAlg (U1,R)) . i ; ::_thesis: x in rng f then consider a1 being set such that A13: a1 in the Sorts of U1 . s and A14: x = Class ((CompClass (R,(CComp s))),a1) by A11, Def10; reconsider a2 = a1 as Element of the Sorts of U1 . s by A13; ( OSClass (R,a2) = x & f . a1 in rng f ) by A10, A13, A14, FUNCT_1:def_3; hence x in rng f by A12, Def21; ::_thesis: verum end; then the Sorts of (QuotOSAlg (U1,R)) . i c= rng f by TARSKI:def_3; hence rng ((OSNat_Hom (U1,R)) . i) = the Sorts of (QuotOSAlg (U1,R)) . i by XBOOLE_0:def_10; ::_thesis: verum end; hence OSNat_Hom (U1,R) is "onto" by MSUALG_3:def_3; ::_thesis: OSNat_Hom (U1,R) is order-sorted thus OSNat_Hom (U1,R) is order-sorted ::_thesis: verum proof reconsider S2 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; let s1, s2 be Element of S; :: according to OSALG_3:def_1 ::_thesis: ( not s1 <= s2 or for b1 being set holds ( not b1 in dom ((OSNat_Hom (U1,R)) . s1) or ( b1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . b1 = ((OSNat_Hom (U1,R)) . s2) . b1 ) ) ) assume A15: s1 <= s2 ; ::_thesis: for b1 being set holds ( not b1 in dom ((OSNat_Hom (U1,R)) . s1) or ( b1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . b1 = ((OSNat_Hom (U1,R)) . s2) . b1 ) ) A16: S2 . s1 c= S2 . s2 by A15, OSALG_1:def_16; let a1 be set ; ::_thesis: ( not a1 in dom ((OSNat_Hom (U1,R)) . s1) or ( a1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1 ) ) assume A17: a1 in dom ((OSNat_Hom (U1,R)) . s1) ; ::_thesis: ( a1 in dom ((OSNat_Hom (U1,R)) . s2) & ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1 ) A18: a1 in the Sorts of U1 . s1 by A17; then reconsider b2 = a1 as Element of the Sorts of U1 . s2 by A16; dom ((OSNat_Hom (U1,R)) . s2) = the Sorts of U1 . s2 by FUNCT_2:def_1; hence a1 in dom ((OSNat_Hom (U1,R)) . s2) by A16, A18; ::_thesis: ((OSNat_Hom (U1,R)) . s1) . a1 = ((OSNat_Hom (U1,R)) . s2) . a1 reconsider b1 = a1 as Element of the Sorts of U1 . s1 by A17; thus ((OSNat_Hom (U1,R)) . 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 .= ((OSNat_Hom (U1,R)) . s2) . a1 by Def22 ; ::_thesis: verum end; end; theorem Th16: :: OSALG_4:16 for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for 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 S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds MSCng F is OSCongruence of U1 let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds MSCng F is OSCongruence of U1 let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies MSCng F is OSCongruence of U1 ) assume that A1: F is_homomorphism U1,U2 and A2: F is order-sorted ; ::_thesis: MSCng F is OSCongruence of U1 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; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) ) assume A3: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) reconsider s3 = s1, s4 = s2 as SortSymbol of S ; let x, y be set ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) ) assume A4: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 ) ; ::_thesis: ( [x,y] in (MSCng F) . s1 iff [x,y] in (MSCng F) . s2 ) 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, MSUALG_4:def_18; ::_thesis: verum end; hence MSCng F is OSCongruence of U1 by Def2; ::_thesis: verum end; definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 23 MSCng F; correctness coherence MSCng F is OSCongruence of U1; by A1, Th16; end; :: deftheorem Def23 defines OSCng OSALG_4:def_23_:_ for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSCng F = MSCng F; definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 24 for x being Element of the Sorts of U1 . s holds it . (OSClass ((OSCng F),x)) = (F . s) . x; existence ex b1 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st for x being Element of the Sorts of U1 . s holds b1 . (OSClass ((OSCng F),x)) = (F . s) . x proof set qa = QuotOSAlg (U1,(OSCng F)); set cqa = the Sorts of (QuotOSAlg (U1,(OSCng F))); set S1 = the Sorts of U1; set S2 = the Sorts of U2; defpred S1[ set , set ] means for a being Element of the Sorts of U1 . s st \$1 = OSClass ((OSCng F),a) holds \$2 = (F . s) . a; A3: the Sorts of (QuotOSAlg (U1,(OSCng F))) . s = OSClass ((OSCng F),s) by Def11; A4: for x being set st x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s holds ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s implies ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) ) assume x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s ; ::_thesis: ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) 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 = a as Element of the Sorts of U1 . s by A5; take y = (F . s) . a; ::_thesis: ( y in the Sorts of U2 . s & S1[x,y] ) thus y in the Sorts of U2 . s ; ::_thesis: S1[x,y] let b be Element of the Sorts of U1 . s; ::_thesis: ( x = OSClass ((OSCng F),b) implies y = (F . s) . b ) assume A7: x = OSClass ((OSCng F),b) ; ::_thesis: y = (F . s) . 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 y = (F . s) . b by MSUALG_4:def_17; ::_thesis: verum end; consider G being Function such that A8: ( dom G = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s & rng G c= the Sorts of U2 . s & ( for x being set st x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s holds S1[x,G . x] ) ) from FUNCT_1:sch_5(A4); reconsider G = G as Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) by A8, FUNCT_2:def_1, RELSET_1:4; take G ; ::_thesis: for x being Element of the Sorts of U1 . s holds G . (OSClass ((OSCng F),x)) = (F . s) . x let a be Element of the Sorts of U1 . s; ::_thesis: G . (OSClass ((OSCng F),a)) = (F . s) . a thus G . (OSClass ((OSCng F),a)) = (F . s) . a by A3, A8; ::_thesis: verum end; uniqueness for b1, b2 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (OSClass ((OSCng F),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass ((OSCng F),x)) = (F . s) . x ) holds b1 = b2 proof set qa = QuotOSAlg (U1,(OSCng F)); set cqa = the Sorts of (QuotOSAlg (U1,(OSCng F))); set u1 = the Sorts of U1; set u2 = the Sorts of U2; let H, G be Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (OSClass ((OSCng F),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (OSClass ((OSCng F),x)) = (F . s) . x ) implies H = G ) assume that A9: for a being Element of the Sorts of U1 . s holds H . (OSClass ((OSCng F),a)) = (F . s) . a and A10: for a being Element of the Sorts of U1 . s holds G . (OSClass ((OSCng F),a)) = (F . s) . a ; ::_thesis: H = G A11: the Sorts of (QuotOSAlg (U1,(OSCng F))) . s = OSClass ((OSCng F),s) by Def11; for x being set st x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s holds H . x = G . x proof let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s implies H . x = G . x ) assume x in the Sorts of (QuotOSAlg (U1,(OSCng F))) . s ; ::_thesis: H . x = G . x 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 the Sorts 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 ; ::_thesis: verum end; hence H = G by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def24 defines OSHomQuot OSALG_4:def_24_:_ for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted holds for b6 being Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . s),( the Sorts of U2 . s) holds ( b6 = OSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b6 . (OSClass ((OSCng F),x)) = (F . s) . x ); definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 25 for s being Element of S holds it . s = OSHomQuot (F,s); existence ex b1 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st for s being Element of S holds b1 . s = OSHomQuot (F,s) proof deffunc H1( Element of S) -> Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . \$1),( the Sorts of U2 . \$1) = OSHomQuot (F,\$1); consider f being Function such that A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider y = x as Element of S ; f . y = OSHomQuot (F,y) by A1; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6; for i being 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 ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . i),( the Sorts of U2 . i) ) assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . i),( the Sorts of U2 . i) then reconsider s = i as Element of S ; f . s = OSHomQuot (F,s) by A1; hence f . i is Function of ( the Sorts of (QuotOSAlg (U1,(OSCng F))) . i),( the Sorts of U2 . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Sorts of (QuotOSAlg (U1,(OSCng F))), the Sorts of U2 by PBOOLE:def_15; reconsider f = f as ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 ; take f ; ::_thesis: for s being Element of S holds f . s = OSHomQuot (F,s) thus for s being Element of S holds f . s = OSHomQuot (F,s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 st ( for s being Element of S holds b1 . s = OSHomQuot (F,s) ) & ( for s being Element of S holds b2 . s = OSHomQuot (F,s) ) holds b1 = b2 proof let H, G be ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2; ::_thesis: ( ( for s being Element of S holds H . s = OSHomQuot (F,s) ) & ( for s being Element of S holds G . s = OSHomQuot (F,s) ) implies H = G ) assume that A2: for s being Element of S holds H . s = OSHomQuot (F,s) and A3: for s being Element of S holds G . s = OSHomQuot (F,s) ; ::_thesis: H = G now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ H_._i_=_G_._i let i be set ; ::_thesis: ( i in the carrier of S implies H . i = G . i ) assume i in the carrier of S ; ::_thesis: H . i = G . i then reconsider s = i as SortSymbol of S ; H . s = OSHomQuot (F,s) by A2; hence H . i = G . i by A3; ::_thesis: verum end; hence H = G by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def25 defines OSHomQuot OSALG_4:def_25_:_ for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 for b5 being ManySortedFunction of (QuotOSAlg (U1,(OSCng F))),U2 holds ( b5 = OSHomQuot F iff for s being Element of S holds b5 . s = OSHomQuot (F,s) ); theorem Th17: :: OSALG_4:17 for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being 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 S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S for F being 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 ) let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being 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 ) let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies ( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted ) ) set mc = OSCng F; set qa = QuotOSAlg (U1,(OSCng F)); set qh = OSHomQuot F; set S1 = the Sorts of U1; assume that A1: F is_homomorphism U1,U2 and A2: F is order-sorted ; ::_thesis: ( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted ) for o being Element of the carrier' of S st Args (o,(QuotOSAlg (U1,(OSCng F)))) <> {} holds for x being Element of Args (o,(QuotOSAlg (U1,(OSCng F)))) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x) proof let o be Element of the carrier' of S; ::_thesis: ( Args (o,(QuotOSAlg (U1,(OSCng F)))) <> {} implies for x being Element of Args (o,(QuotOSAlg (U1,(OSCng F)))) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x) ) assume Args (o,(QuotOSAlg (U1,(OSCng F)))) <> {} ; ::_thesis: for x being Element of Args (o,(QuotOSAlg (U1,(OSCng F)))) holds ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x) let x be Element of Args (o,(QuotOSAlg (U1,(OSCng F)))); ::_thesis: ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x) reconsider o1 = o as OperSymbol of S ; set ro = the_result_sort_of o; set ar = the_arity_of o; A3: dom x = dom (the_arity_of o) by MSUALG_3:6; Args (o,(QuotOSAlg (U1,(OSCng F)))) = (((OSClass (OSCng F)) #) * the Arity of S) . o by MSUALG_1:def_4; then consider a being Element of Args (o,U1) such that A4: x = (OSCng F) #_os a by Th14; A5: dom a = dom (the_arity_of o) by MSUALG_3:6; A6: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_ ((OSHomQuot_F)_#_x)_._y_=_(F_#_a)_._y let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((OSHomQuot F) # x) . y = (F # a) . y ) assume A7: y in dom (the_arity_of o) ; ::_thesis: ((OSHomQuot F) # x) . y = (F # a) . y then reconsider n = y as Nat ; (the_arity_of o) . n in rng (the_arity_of o) by A7, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . n as SortSymbol of S ; A8: (the_arity_of o) /. n = (the_arity_of o) . n by A7, PARTFUN1:def_6; then consider an being Element of the Sorts of U1 . s such that A9: an = a . n and A10: x . n = OSClass ((OSCng F),an) by A4, A7, Def13; ((OSHomQuot F) # x) . n = ((OSHomQuot F) . s) . (x . n) by A3, A7, A8, MSUALG_3:def_6 .= (OSHomQuot (F,s)) . (OSClass ((OSCng F),an)) by A10, Def25 .= (F . s) . an by A1, A2, Def24 .= (F # a) . n by A5, A7, A8, A9, MSUALG_3:def_6 ; hence ((OSHomQuot F) # x) . y = (F # a) . y ; ::_thesis: verum end; o in the carrier' of S ; then o in dom ( the Sorts of U1 * 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 . (the_result_sort_of o) by MSUALG_1:def_2 ; then ( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) by MSUALG_1:def_5; then rng (Den (o,U1)) c= dom (OSQuotRes ((OSCng F),o)) by A11, FUNCT_2:def_1; then A12: ( dom (Den (o,U1)) = Args (o,U1) & dom ((OSQuotRes ((OSCng F),o)) * (Den (o,U1))) = dom (Den (o,U1)) ) by FUNCT_2:def_1, RELAT_1:27; the_arity_of o = the Arity of S . o by MSUALG_1:def_1; then A13: product ((OSClass (OSCng F)) * (the_arity_of o)) = (((OSClass (OSCng F)) #) * the Arity of S) . o by MSAFREE:1; reconsider da = (Den (o,U1)) . a as Element of the Sorts of U1 . (the_result_sort_of o) by A11, MSUALG_1:def_5; A14: (OSHomQuot F) . (the_result_sort_of o) = OSHomQuot (F,(the_result_sort_of o)) by Def25; Den (o,(QuotOSAlg (U1,(OSCng F)))) = (OSQuotCharact (OSCng F)) . o by MSUALG_1:def_6 .= OSQuotCharact ((OSCng F),o1) by Def19 ; then (Den (o,(QuotOSAlg (U1,(OSCng F))))) . x = ((OSQuotRes ((OSCng F),o)) * (Den (o,U1))) . a by A4, A13, Def18 .= (OSQuotRes ((OSCng F),o)) . da by A12, FUNCT_1:12 .= OSClass ((OSCng F),da) by Def14 ; then A15: ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (F . (the_result_sort_of o)) . ((Den (o,U1)) . a) by A1, A2, A14, Def24 .= (Den (o,U2)) . (F # a) by A1, MSUALG_3:def_7 ; ( dom ((OSHomQuot F) # x) = dom (the_arity_of o) & dom (F # a) = dom (the_arity_of o) ) by MSUALG_3:6; hence ((OSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,(OSCng F))))) . x) = (Den (o,U2)) . ((OSHomQuot F) # x) by A6, A15, FUNCT_1:2; ::_thesis: verum end; hence OSHomQuot F is_homomorphism QuotOSAlg (U1,(OSCng F)),U2 by MSUALG_3:def_7; :: according to MSUALG_3:def_9 ::_thesis: ( OSHomQuot F is "1-1" & OSHomQuot F is order-sorted ) for i being set st i in the carrier of S holds (OSHomQuot F) . i is one-to-one proof let i be set ; ::_thesis: ( i in the carrier of S implies (OSHomQuot F) . i is one-to-one ) set f = (OSHomQuot F) . i; assume i in the carrier of S ; ::_thesis: (OSHomQuot F) . i is one-to-one then reconsider s = i as SortSymbol of S ; A16: (OSHomQuot F) . i = OSHomQuot (F,s) by Def25; for x1, x2 being set st x1 in dom ((OSHomQuot F) . i) & x2 in dom ((OSHomQuot F) . i) & ((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom ((OSHomQuot F) . i) & x2 in dom ((OSHomQuot F) . i) & ((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 implies x1 = x2 ) assume that A17: x1 in dom ((OSHomQuot F) . i) and A18: x2 in dom ((OSHomQuot F) . i) and A19: ((OSHomQuot F) . i) . x1 = ((OSHomQuot F) . i) . x2 ; ::_thesis: x1 = x2 x2 in (OSClass (OSCng F)) . s by A16, A18, FUNCT_2:def_1; then x2 in OSClass ((OSCng F),s) by Def11; then consider a2 being set such that A20: a2 in the Sorts of U1 . s and A21: x2 = Class ((CompClass ((OSCng F),(CComp s))),a2) by Def10; reconsider a2 = a2 as Element of the Sorts of U1 . s by A20; A22: x2 = OSClass ((OSCng F),a2) by A21; x1 in (OSClass (OSCng F)) . s by A16, A17, FUNCT_2:def_1; then x1 in OSClass ((OSCng F),s) by Def11; then consider a1 being set such that A23: a1 in the Sorts of U1 . s and A24: x1 = Class ((CompClass ((OSCng F),(CComp s))),a1) by Def10; reconsider a1 = a1 as Element of the Sorts of U1 . s by A23; ( (F . s) . a1 = ((OSHomQuot F) . i) . (OSClass ((OSCng F),a1)) & (F . s) . a2 = ((OSHomQuot F) . i) . (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 x1 = x2 by A22, A25, Th12; ::_thesis: verum end; hence (OSHomQuot F) . i is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; hence OSHomQuot F is "1-1" by MSUALG_3:1; ::_thesis: OSHomQuot F is order-sorted thus OSHomQuot F is order-sorted ::_thesis: verum proof reconsider S1O = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; reconsider sqa = the Sorts of (QuotOSAlg (U1,(OSCng F))) as OrderSortedSet of S ; let s1, s2 be Element of S; :: according to OSALG_3:def_1 ::_thesis: ( not s1 <= s2 or for b1 being set holds ( not b1 in dom ((OSHomQuot F) . s1) or ( b1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . b1 = ((OSHomQuot F) . s2) . b1 ) ) ) assume A26: s1 <= s2 ; ::_thesis: for b1 being set holds ( not b1 in dom ((OSHomQuot F) . s1) or ( b1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . b1 = ((OSHomQuot F) . s2) . b1 ) ) let a1 be set ; ::_thesis: ( not a1 in dom ((OSHomQuot F) . s1) or ( a1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1 ) ) assume A27: a1 in dom ((OSHomQuot F) . s1) ; ::_thesis: ( a1 in dom ((OSHomQuot F) . s2) & ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1 ) 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 the Sorts of U1 . 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 the Sorts of U1 . s2 by A28; A30: a1 = OSClass ((OSCng F),x2) by A26, A29, Th4; reconsider s3 = s1, s4 = s2 as Element of S ; A31: ( dom ((OSHomQuot F) . s1) = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s1 & dom ((OSHomQuot F) . s2) = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s2 ) by FUNCT_2:def_1; reconsider x1 = x as Element of the Sorts of U1 . 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 ((OSHomQuot F) . s2) by A27, A31; ::_thesis: ((OSHomQuot F) . s1) . a1 = ((OSHomQuot F) . s2) . a1 thus ((OSHomQuot F) . 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 .= ((OSHomQuot F) . s2) . a1 by A30, Def25 ; ::_thesis: verum end; end; theorem Th18: :: OSALG_4:18 for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being 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 S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 & F is order-sorted implies OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 ) set mc = OSCng F; set qa = QuotOSAlg (U1,(OSCng F)); set qh = OSHomQuot F; assume that A1: F is_epimorphism U1,U2 and A2: F is order-sorted ; ::_thesis: OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 set Sq = the Sorts of (QuotOSAlg (U1,(OSCng F))); set S1 = the Sorts of U1; set 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 being set st i in the carrier of S holds rng ((OSHomQuot F) . i) = the Sorts of U2 . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng ((OSHomQuot F) . i) = the Sorts of U2 . i ) set f = (OSHomQuot F) . i; assume i in the carrier of S ; ::_thesis: rng ((OSHomQuot F) . i) = the Sorts of U2 . i then reconsider s = i as SortSymbol of S ; A5: rng (F . s) = the Sorts of U2 . s by A4, MSUALG_3:def_3; A6: (OSHomQuot F) . i = OSHomQuot (F,s) by Def25; then A7: dom ((OSHomQuot F) . i) = the Sorts of (QuotOSAlg (U1,(OSCng F))) . s by FUNCT_2:def_1; thus rng ((OSHomQuot F) . i) c= the Sorts of U2 . i by A6, RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of U2 . i c= rng ((OSHomQuot F) . i) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of U2 . i or x in rng ((OSHomQuot F) . i) ) assume x in the Sorts of U2 . i ; ::_thesis: x in rng ((OSHomQuot F) . i) then consider a being set such that A8: a in dom (F . s) and A9: (F . s) . a = x by A5, FUNCT_1:def_3; A10: the Sorts of (QuotOSAlg (U1,(OSCng F))) . s = OSClass ((OSCng F),s) by Def11; reconsider a = a as Element of the Sorts of U1 . s by A8; ((OSHomQuot F) . i) . (OSClass ((OSCng F),a)) = x by A2, A3, A6, A9, Def24; hence x in rng ((OSHomQuot F) . i) by A7, A10, FUNCT_1:def_3; ::_thesis: verum end; then A11: OSHomQuot F is "onto" by MSUALG_3:def_3; OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 by A2, A3, Th17; then ( OSHomQuot F is_homomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is "1-1" ) by MSUALG_3:def_9; hence OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 by A11, MSUALG_3:13; ::_thesis: verum end; theorem :: OSALG_4:19 for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic proof let S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 & F is order-sorted implies QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic ) assume ( F is_epimorphism U1,U2 & F is order-sorted ) ; ::_thesis: QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic then OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 by Th18; hence QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic by MSUALG_3:def_11; ::_thesis: verum end; definition let S be OrderSortedSign; let U1 be non-empty OSAlgebra of S; let R be MSEquivalence-like OrderSortedRelation of U1; attrR is monotone means :Def26: :: OSALG_4:def 26 for o1, o2 being OperSymbol of S st o1 <= o2 holds 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; :: deftheorem Def26 defines monotone OSALG_4:def_26_:_ for S being OrderSortedSign for U1 being non-empty OSAlgebra of S for R being MSEquivalence-like OrderSortedRelation of U1 holds ( R is monotone iff for o1, o2 being OperSymbol of S st o1 <= o2 holds 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) ); theorem Th20: :: OSALG_4:20 for S being OrderSortedSign for 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; ::_thesis: for U1 being non-empty OSAlgebra of S holds [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1 let U1 be non-empty OSAlgebra of S; ::_thesis: [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1 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; :: according to OSALG_4:def_1 ::_thesis: ( s1 <= s2 implies for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in C . s1 iff [x,y] in C . s2 ) ) assume A1: s1 <= s2 ; ::_thesis: for x, y being set st x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 holds ( [x,y] in C . s1 iff [x,y] in C . 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 ; ::_thesis: ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 implies ( [x,y] in C . s1 iff [x,y] in C . s2 ) ) assume ( x in the Sorts of U1 . s1 & y in the Sorts of U1 . s1 ) ; ::_thesis: ( [x,y] in C . s1 iff [x,y] in C . s2 ) hence ( [x,y] in C . s1 iff [x,y] in C . s2 ) by A2, A3, ZFMISC_1:87; ::_thesis: verum end; hence [| the Sorts of U1, the Sorts of U1|] is OSCongruence of U1 by Def2; ::_thesis: verum end; theorem Th21: :: OSALG_4:21 for S being OrderSortedSign for U1 being non-empty OSAlgebra of S for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds R is monotone proof let S be OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds R is monotone let U1 be non-empty OSAlgebra of S; ::_thesis: for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds R is monotone let R be OSCongruence of U1; ::_thesis: ( R = [| the Sorts of U1, the Sorts of U1|] implies R is monotone ) assume A1: R = [| the Sorts of U1, the Sorts of U1|] ; ::_thesis: R is monotone reconsider O1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; let o1, o2 be OperSymbol of S; :: according to OSALG_4:def_26 ::_thesis: ( o1 <= o2 implies 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) ) assume A2: o1 <= o2 ; ::_thesis: 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) set s2 = the_result_sort_of o2; set s1 = the_result_sort_of o1; the_result_sort_of o1 <= the_result_sort_of o2 by A2, OSALG_1:def_20; then A3: O1 . (the_result_sort_of o1) c= O1 . (the_result_sort_of o2) by OSALG_1:def_16; let x1 be Element of Args (o1,U1); ::_thesis: 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) let x2 be Element of Args (o2,U1); ::_thesis: ( ( for y being Nat st y in dom x1 holds [(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) ) assume for y being Nat st y in dom x1 holds [(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ; ::_thesis: [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) A4: ( (Den (o1,U1)) . x1 in the Sorts of U1 . (the_result_sort_of o1) & (Den (o2,U1)) . x2 in the Sorts of U1 . (the_result_sort_of o2) ) by MSUALG_9:18; R . (the_result_sort_of o2) = [:( the Sorts of U1 . (the_result_sort_of o2)),( the Sorts of U1 . (the_result_sort_of o2)):] by A1, PBOOLE:def_16; hence [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by A3, A4, ZFMISC_1:87; ::_thesis: verum end; registration let S be OrderSortedSign; let U1 be non-empty OSAlgebra of S; cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like monotone for OrderSortedRelation of U1; existence ex b1 being OSCongruence of U1 st b1 is monotone proof reconsider R = [| the Sorts of U1, the Sorts of U1|] as OSCongruence of U1 by Th20; take R ; ::_thesis: R is monotone thus R is monotone by Th21; ::_thesis: verum end; end; registration let S be OrderSortedSign; let U1 be non-empty OSAlgebra of S; cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like monotone for OrderSortedRelation of U1; existence ex b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone proof set R = the monotone OSCongruence of U1; take the monotone OSCongruence of U1 ; ::_thesis: the monotone OSCongruence of U1 is monotone thus the monotone OSCongruence of U1 is monotone ; ::_thesis: verum end; end; theorem Th22: :: OSALG_4:22 for S being OrderSortedSign for U1 being non-empty OSAlgebra of S for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like proof let S be OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like let U1 be non-empty OSAlgebra of S; ::_thesis: for R being MSEquivalence-like monotone OrderSortedRelation of U1 holds R is MSCongruence-like let R be MSEquivalence-like monotone OrderSortedRelation of U1; ::_thesis: R is MSCongruence-like for o being Element of the carrier' of S for x, y being Element of Args (o,U1) st ( for n being 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 R is MSCongruence-like by MSUALG_4:def_4; ::_thesis: verum end; registration let S be OrderSortedSign; let U1 be non-empty OSAlgebra of S; cluster MSEquivalence-like monotone -> MSEquivalence-like MSCongruence-like for OrderSortedRelation of U1; coherence for b1 being MSEquivalence-like OrderSortedRelation of U1 st b1 is monotone holds b1 is MSCongruence-like by Th22; end; theorem Th23: :: OSALG_4:23 for S being OrderSortedSign for U1 being non-empty monotone OSAlgebra of S for R being OSCongruence of U1 holds R is monotone proof let S be OrderSortedSign; ::_thesis: for U1 being non-empty monotone OSAlgebra of S for R being OSCongruence of U1 holds R is monotone let U1 be non-empty monotone OSAlgebra of S; ::_thesis: for R being OSCongruence of U1 holds R is monotone let R be OSCongruence of U1; ::_thesis: R is monotone let o1, o2 be OperSymbol of S; :: according to OSALG_4:def_26 ::_thesis: ( o1 <= o2 implies 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) ) assume A1: o1 <= o2 ; ::_thesis: 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) let x1 be Element of Args (o1,U1); ::_thesis: 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) 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); ::_thesis: ( ( for y being Nat st y in dom x1 holds [(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) ) assume for y being Nat st y in dom x1 holds [(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ; ::_thesis: [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) 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 [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in R . (the_result_sort_of o2) by A2, A3, GRFUNC_1:2; ::_thesis: verum end; registration let S be OrderSortedSign; let U1 be non-empty monotone OSAlgebra of S; cluster MSEquivalence-like MSCongruence-like -> monotone for OrderSortedRelation of U1; coherence for b1 being OSCongruence of U1 holds b1 is monotone by Th23; end; registration let S be locally_directed OrderSortedSign; let U1 be non-empty OSAlgebra of S; let R be monotone OSCongruence of U1; cluster QuotOSAlg (U1,R) -> monotone ; coherence QuotOSAlg (U1,R) is monotone 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; :: according to OSALG_1:def_21 ::_thesis: ( not o1 <= o2 or (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R))) ) assume A1: o1 <= o2 ; ::_thesis: (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R))) A2: Args (o1,(QuotOSAlg (U1,R))) c= Args (o2,(QuotOSAlg (U1,R))) by A1, OSALG_1:26; Den (o2,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o2 by MSUALG_1:def_6; then A3: Den (o2,(QuotOSAlg (U1,R))) = 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,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o1 by MSUALG_1:def_6; then A5: Den (o1,(QuotOSAlg (U1,R))) = 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,(QuotOSAlg (U1,R)))) holds (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x proof let x be set ; ::_thesis: ( x in dom (Den (o1,(QuotOSAlg (U1,R)))) implies (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x ) assume x in dom (Den (o1,(QuotOSAlg (U1,R)))) ; ::_thesis: (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x then A12: x in Args (o1,(QuotOSAlg (U1,R))) ; 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,(QuotOSAlg (U1,R))) 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; ::_thesis: ( y in dom a1 implies [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y) ) assume A19: y in dom a1 ; ::_thesis: [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y) 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 [(a1 . y),(a2 . y)] in R . ((the_arity_of o2) /. y) by A21, A26, Th12; ::_thesis: verum 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 (Den (o1,(QuotOSAlg (U1,R)))) . x = (Den (o2,(QuotOSAlg (U1,R)))) . x by A5, A3, A17, A14, A18, A16, A15, A29, Def18; ::_thesis: verum end; ( dom (Den (o2,(QuotOSAlg (U1,R)))) = Args (o2,(QuotOSAlg (U1,R))) & dom (Den (o1,(QuotOSAlg (U1,R)))) = Args (o1,(QuotOSAlg (U1,R))) ) by FUNCT_2:def_1; then dom (Den (o1,(QuotOSAlg (U1,R)))) = (dom (Den (o2,(QuotOSAlg (U1,R))))) /\ (Args (o1,(QuotOSAlg (U1,R)))) by A2, XBOOLE_1:28; hence (Den (o2,(QuotOSAlg (U1,R)))) | (Args (o1,(QuotOSAlg (U1,R)))) = Den (o1,(QuotOSAlg (U1,R))) by A11, FUNCT_1:46; ::_thesis: verum end; end; theorem :: OSALG_4:24 for S being locally_directed OrderSortedSign for U1 being non-empty OSAlgebra of S for U2 being non-empty monotone OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSCng F is monotone proof let S be locally_directed OrderSortedSign; ::_thesis: for U1 being non-empty OSAlgebra of S for U2 being non-empty monotone OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSCng F is monotone let U1 be non-empty OSAlgebra of S; ::_thesis: for U2 being non-empty monotone OSAlgebra of S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSCng F is monotone let U2 be non-empty monotone OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSCng F is monotone let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies OSCng F is monotone ) assume that A1: F is_homomorphism U1,U2 and A2: F is order-sorted ; ::_thesis: OSCng F is monotone reconsider S1 = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; set O1 = the Sorts of U1; let o1, o2 be OperSymbol of S; :: according to OSALG_4:def_26 ::_thesis: ( o1 <= o2 implies 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 (OSCng F) . ((the_arity_of o2) /. y) ) holds [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) ) assume A3: o1 <= o2 ; ::_thesis: 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 (OSCng F) . ((the_arity_of o2) /. y) ) holds [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) A4: (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) by A3, OSALG_1:def_21; set R = OSCng F; set rs1 = the_result_sort_of o1; set rs2 = the_result_sort_of o2; let x1 be Element of Args (o1,U1); ::_thesis: for x2 being Element of Args (o2,U1) st ( for y being Nat st y in dom x1 holds [(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) holds [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) let x2 be Element of Args (o2,U1); ::_thesis: ( ( for y being Nat st y in dom x1 holds [(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ) implies [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) ) assume A5: for y being Nat st y in dom x1 holds [(x1 . y),(x2 . y)] in (OSCng F) . ((the_arity_of o2) /. y) ; ::_thesis: [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) 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; set D2 = (Den (o2,U1)) . x2; set M = MSCng F; A6: (Den (o1,U1)) . x1 in S1 . (the_result_sort_of o1) 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: the_result_sort_of o1 <= the_result_sort_of o2 by A3, OSALG_1:def_20; then S1 . (the_result_sort_of o1) c= S1 . (the_result_sort_of o2) by OSALG_1:def_16; then reconsider D11 = (Den (o1,U1)) . x1, D12 = (Den (o2,U1)) . x12 as Element of the Sorts of U1 . (the_result_sort_of o2) by A6, MSUALG_9:18; (Den (o1,U1)) . x1 in dom (F . (the_result_sort_of o1)) by A6, FUNCT_2:def_1; then (F . (the_result_sort_of o2)) . ((Den (o1,U1)) . x1) = (F . (the_result_sort_of o1)) . ((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 . (the_result_sort_of o2)) . ((Den (o2,U1)) . x12) by A1, MSUALG_3:def_7 ; then A9: ( (Den (o2,U1)) . x2 in the Sorts of U1 . (the_result_sort_of o2) & [D11,D12] in MSCng (F,(the_result_sort_of o2)) ) by MSUALG_4:def_17, MSUALG_9:18; field ((OSCng F) . (the_result_sort_of o2)) = the Sorts of U1 . (the_result_sort_of o2) by ORDERS_1:12; then A10: (OSCng F) . (the_result_sort_of o2) is_transitive_in the Sorts of U1 . (the_result_sort_of o2) by RELAT_2:def_16; A11: [((Den (o2,U1)) . x12),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) by A5, MSUALG_4:def_4; ( (MSCng F) . (the_result_sort_of o2) = MSCng (F,(the_result_sort_of o2)) & MSCng F = OSCng F ) by A1, A2, Def23, MSUALG_4:def_18; hence [((Den (o1,U1)) . x1),((Den (o2,U1)) . x2)] in (OSCng F) . (the_result_sort_of o2) by A11, A9, A10, RELAT_2:def_8; ::_thesis: verum end; definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 27 for x being Element of the Sorts of U1 . s holds it . (OSClass (R,x)) = (F . s) . x; existence ex b1 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st for x being Element of the Sorts of U1 . s holds b1 . (OSClass (R,x)) = (F . s) . x proof set qa = QuotOSAlg (U1,R); set cqa = the Sorts of (QuotOSAlg (U1,R)); set S1 = the Sorts of U1; set S2 = the Sorts of U2; defpred S1[ set , set ] means for a being Element of the Sorts of U1 . s st \$1 = OSClass (R,a) holds \$2 = (F . s) . a; A4: the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s) by Def11; A5: for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . s holds ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,R)) . s implies ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) ) A6: R . s c= (OSCng F) . s by A3, PBOOLE:def_2; assume x in the Sorts of (QuotOSAlg (U1,R)) . s ; ::_thesis: ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) 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 = a as Element of the Sorts of U1 . s by A7; take y = (F . s) . a; ::_thesis: ( y in the Sorts of U2 . s & S1[x,y] ) thus y in the Sorts of U2 . s ; ::_thesis: S1[x,y] let b be Element of the Sorts of U1 . s; ::_thesis: ( x = OSClass (R,b) implies y = (F . s) . b ) assume A9: x = OSClass (R,b) ; ::_thesis: y = (F . s) . 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 y = (F . s) . b by MSUALG_4:def_17; ::_thesis: verum end; consider G being Function such that A10: ( dom G = the Sorts of (QuotOSAlg (U1,R)) . s & rng G c= the Sorts of U2 . s & ( for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . s holds S1[x,G . x] ) ) from FUNCT_1:sch_5(A5); reconsider G = G as Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) by A10, FUNCT_2:def_1, RELSET_1:4; take G ; ::_thesis: for x being Element of the Sorts of U1 . s holds G . (OSClass (R,x)) = (F . s) . x let a be Element of the Sorts of U1 . s; ::_thesis: G . (OSClass (R,a)) = (F . s) . a thus G . (OSClass (R,a)) = (F . s) . a by A4, A10; ::_thesis: verum end; uniqueness for b1, b2 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (OSClass (R,x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (OSClass (R,x)) = (F . s) . x ) holds b1 = b2 proof set qa = QuotOSAlg (U1,R); set cqa = the Sorts of (QuotOSAlg (U1,R)); set u1 = the Sorts of U1; set u2 = the Sorts of U2; let H, G be Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (OSClass (R,x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (OSClass (R,x)) = (F . s) . x ) implies H = G ) assume that A11: for a being Element of the Sorts of U1 . s holds H . (OSClass (R,a)) = (F . s) . a and A12: for a being Element of the Sorts of U1 . s holds G . (OSClass (R,a)) = (F . s) . a ; ::_thesis: H = G A13: the Sorts of (QuotOSAlg (U1,R)) . s = OSClass (R,s) by Def11; for x being set st x in the Sorts of (QuotOSAlg (U1,R)) . s holds H . x = G . x proof let x be set ; ::_thesis: ( x in the Sorts of (QuotOSAlg (U1,R)) . s implies H . x = G . x ) assume x in the Sorts of (QuotOSAlg (U1,R)) . s ; ::_thesis: H . x = G . x 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 the Sorts 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 ; ::_thesis: verum end; hence H = G by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def27 defines OSHomQuot OSALG_4:def_27_:_ for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 for R being OSCongruence of U1 for s being Element of S st F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F holds for b7 being Function of ( the Sorts of (QuotOSAlg (U1,R)) . s),( the Sorts of U2 . s) holds ( b7 = OSHomQuot (F,R,s) iff for x being Element of the Sorts of U1 . s holds b7 . (OSClass (R,x)) = (F . s) . x ); definition let S be locally_directed OrderSortedSign; 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: :: OSALG_4:def 28 for s being Element of S holds it . s = OSHomQuot (F,R,s); existence ex b1 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st for s being Element of S holds b1 . s = OSHomQuot (F,R,s) proof deffunc H1( Element of S) -> Function of ( the Sorts of (QuotOSAlg (U1,R)) . \$1),( the Sorts of U2 . \$1) = OSHomQuot (F,R,\$1); consider f being Function such that A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider y = x as Element of S ; f . y = OSHomQuot (F,R,y) by A1; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6; for i being 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 ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i) ) assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i) then reconsider s = i as Element of S ; f . s = OSHomQuot (F,R,s) by A1; hence f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Sorts of (QuotOSAlg (U1,R)), the Sorts of U2 by PBOOLE:def_15; reconsider f = f as ManySortedFunction of (QuotOSAlg (U1,R)),U2 ; take f ; ::_thesis: for s being Element of S holds f . s = OSHomQuot (F,R,s) thus for s being Element of S holds f . s = OSHomQuot (F,R,s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 st ( for s being Element of S holds b1 . s = OSHomQuot (F,R,s) ) & ( for s being Element of S holds b2 . s = OSHomQuot (F,R,s) ) holds b1 = b2 proof let H, G be ManySortedFunction of (QuotOSAlg (U1,R)),U2; ::_thesis: ( ( for s being Element of S holds H . s = OSHomQuot (F,R,s) ) & ( for s being Element of S holds G . s = OSHomQuot (F,R,s) ) implies H = G ) assume that A2: for s being Element of S holds H . s = OSHomQuot (F,R,s) and A3: for s being Element of S holds G . s = OSHomQuot (F,R,s) ; ::_thesis: H = G now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ H_._i_=_G_._i let i be set ; ::_thesis: ( i in the carrier of S implies H . i = G . i ) assume i in the carrier of S ; ::_thesis: H . i = G . i then reconsider s = i as SortSymbol of S ; H . s = OSHomQuot (F,R,s) by A2; hence H . i = G . i by A3; ::_thesis: verum end; hence H = G by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def28 defines OSHomQuot OSALG_4:def_28_:_ for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 for R being OSCongruence of U1 for b6 being ManySortedFunction of (QuotOSAlg (U1,R)),U2 holds ( b6 = OSHomQuot (F,R) iff for s being Element of S holds b6 . s = OSHomQuot (F,R,s) ); theorem :: OSALG_4:25 for S being locally_directed OrderSortedSign for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 for R being 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 S be locally_directed OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S for F being ManySortedFunction of U1,U2 for R being 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 ) let U1, U2 be non-empty OSAlgebra of S; ::_thesis: for F being ManySortedFunction of U1,U2 for R being 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 ) let F be ManySortedFunction of U1,U2; ::_thesis: for R being 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 ) let R be OSCongruence of U1; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted & R c= OSCng F implies ( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted ) ) set mc = R; set qa = QuotOSAlg (U1,R); set qh = OSHomQuot (F,R); set 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 ; ::_thesis: ( OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot (F,R) is order-sorted ) for o being Element of the carrier' of S st Args (o,(QuotOSAlg (U1,R))) <> {} holds for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) proof let o be Element of the carrier' of S; ::_thesis: ( Args (o,(QuotOSAlg (U1,R))) <> {} implies for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) ) assume Args (o,(QuotOSAlg (U1,R))) <> {} ; ::_thesis: for x being Element of Args (o,(QuotOSAlg (U1,R))) holds ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) let x be Element of Args (o,(QuotOSAlg (U1,R))); ::_thesis: ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) reconsider o1 = o as OperSymbol of S ; set ro = the_result_sort_of o; set ar = the_arity_of o; A4: dom x = dom (the_arity_of o) by MSUALG_3:6; Args (o,(QuotOSAlg (U1,R))) = (((OSClass R) #) * the Arity of S) . o by MSUALG_1:def_4; then consider a being Element of Args (o,U1) such that A5: x = R #_os a by Th14; A6: dom a = dom (the_arity_of o) by MSUALG_3:6; A7: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_ ((OSHomQuot_(F,R))_#_x)_._y_=_(F_#_a)_._y let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((OSHomQuot (F,R)) # x) . y = (F # a) . y ) assume A8: y in dom (the_arity_of o) ; ::_thesis: ((OSHomQuot (F,R)) # x) . y = (F # a) . y then reconsider n = y as Nat ; (the_arity_of o) . n in rng (the_arity_of o) by A8, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . n as SortSymbol of S ; A9: (the_arity_of o) /. n = (the_arity_of o) . n by A8, PARTFUN1:def_6; then consider an being Element of the Sorts of U1 . s such that A10: an = a . n and A11: x . n = OSClass (R,an) by A5, A8, Def13; ((OSHomQuot (F,R)) # x) . n = ((OSHomQuot (F,R)) . s) . (x . n) by A4, A8, A9, MSUALG_3:def_6 .= (OSHomQuot (F,R,s)) . (OSClass (R,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 ((OSHomQuot (F,R)) # x) . y = (F # a) . y ; ::_thesis: verum end; o in the carrier' of S ; then o in dom ( the Sorts of U1 * 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 . (the_result_sort_of o) by MSUALG_1:def_2 ; then ( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) by MSUALG_1:def_5; then rng (Den (o,U1)) c= dom (OSQuotRes (R,o)) by A12, FUNCT_2:def_1; then A13: ( 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; the_arity_of o = the Arity of S . o by MSUALG_1:def_1; then A14: product ((OSClass R) * (the_arity_of o)) = (((OSClass R) #) * the Arity of S) . o by MSAFREE:1; reconsider da = (Den (o,U1)) . a as Element of the Sorts of U1 . (the_result_sort_of o) by A12, MSUALG_1:def_5; A15: (OSHomQuot (F,R)) . (the_result_sort_of o) = OSHomQuot (F,R,(the_result_sort_of o)) by Def28; Den (o,(QuotOSAlg (U1,R))) = (OSQuotCharact R) . o by MSUALG_1:def_6 .= OSQuotCharact (R,o1) by Def19 ; then (Den (o,(QuotOSAlg (U1,R)))) . x = ((OSQuotRes (R,o)) * (Den (o,U1))) . a by A5, A14, Def18 .= (OSQuotRes (R,o)) . da by A13, FUNCT_1:12 .= OSClass (R,da) by Def14 ; then A16: ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (F . (the_result_sort_of o)) . ((Den (o,U1)) . a) by A1, A2, A3, A15, Def27 .= (Den (o,U2)) . (F # a) by A1, MSUALG_3:def_7 ; ( dom ((OSHomQuot (F,R)) # x) = dom (the_arity_of o) & dom (F # a) = dom (the_arity_of o) ) by MSUALG_3:6; hence ((OSHomQuot (F,R)) . (the_result_sort_of o)) . ((Den (o,(QuotOSAlg (U1,R)))) . x) = (Den (o,U2)) . ((OSHomQuot (F,R)) # x) by A7, A16, FUNCT_1:2; ::_thesis: verum end; hence OSHomQuot (F,R) is_homomorphism QuotOSAlg (U1,R),U2 by MSUALG_3:def_7; ::_thesis: OSHomQuot (F,R) is order-sorted thus OSHomQuot (F,R) is order-sorted ::_thesis: verum proof reconsider S1O = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17; reconsider sqa = the Sorts of (QuotOSAlg (U1,R)) as OrderSortedSet of S ; let s1, s2 be Element of S; :: according to OSALG_3:def_1 ::_thesis: ( not s1 <= s2 or for b1 being set holds ( not b1 in dom ((OSHomQuot (F,R)) . s1) or ( b1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . b1 = ((OSHomQuot (F,R)) . s2) . b1 ) ) ) assume A17: s1 <= s2 ; ::_thesis: for b1 being set holds ( not b1 in dom ((OSHomQuot (F,R)) . s1) or ( b1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . b1 = ((OSHomQuot (F,R)) . s2) . b1 ) ) let a1 be set ; ::_thesis: ( not a1 in dom ((OSHomQuot (F,R)) . s1) or ( a1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1 ) ) assume A18: a1 in dom ((OSHomQuot (F,R)) . s1) ; ::_thesis: ( a1 in dom ((OSHomQuot (F,R)) . s2) & ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1 ) 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 the Sorts of U1 . 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 the Sorts of U1 . s2 by A19; A21: a1 = OSClass (R,x2) by A17, A20, Th4; reconsider s3 = s1, s4 = s2 as Element of S ; A22: ( dom ((OSHomQuot (F,R)) . s1) = the Sorts of (QuotOSAlg (U1,R)) . s1 & dom ((OSHomQuot (F,R)) . s2) = the Sorts of (QuotOSAlg (U1,R)) . s2 ) by FUNCT_2:def_1; reconsider x1 = x as Element of the Sorts of U1 . 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 ((OSHomQuot (F,R)) . s2) by A18, A22; ::_thesis: ((OSHomQuot (F,R)) . s1) . a1 = ((OSHomQuot (F,R)) . s2) . a1 thus ((OSHomQuot (F,R)) . 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 .= ((OSHomQuot (F,R)) . s2) . a1 by A21, Def28 ; ::_thesis: verum end; end;