:: MSUALG_4 semantic presentation begin registration let I be set ; cluster Relation-like I -defined Function-like total Relation-yielding for set ; existence ex b1 being ManySortedSet of I st b1 is Relation-yielding proof set R = the Relation; set f = I --> the Relation; reconsider f = I --> the Relation as ManySortedSet of I ; 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 I be set ; let A, B be ManySortedSet of I; mode ManySortedRelation of A,B -> ManySortedSet of I means :Def1: :: MSUALG_4:def 1 for i being set st i in I holds it . i is Relation of (A . i),(B . i); existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i is Relation of (A . i),(B . i) proof consider R being Relation such that A1: R = {} ; set f = I --> R; reconsider f = I --> R as ManySortedSet of I ; take f ; ::_thesis: for i being set st i in I holds f . i is Relation of (A . i),(B . i) for i being set st i in I holds f . i is Relation of (A . i),(B . i) proof let i be set ; ::_thesis: ( i in I implies f . i is Relation of (A . i),(B . i) ) assume i in I ; ::_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; hence for i being set st i in I holds f . i is Relation of (A . i),(B . i) ; ::_thesis: verum end; end; :: deftheorem Def1 defines ManySortedRelation MSUALG_4:def_1_:_ for I being set for A, B, b4 being ManySortedSet of I holds ( b4 is ManySortedRelation of A,B iff for i being set st i in I holds b4 . i is Relation of (A . i),(B . i) ); registration let I be set ; let A, B be ManySortedSet of I; cluster -> Relation-yielding for ManySortedRelation of A,B; coherence for b1 being ManySortedRelation of A,B holds b1 is Relation-yielding proof let R be ManySortedRelation of A,B; ::_thesis: R is Relation-yielding let x be set ; :: according to FUNCOP_1:def_11 ::_thesis: ( not x in dom R or R . x is set ) assume x in dom R ; ::_thesis: R . x is set then x in I ; hence R . x is set by Def1; ::_thesis: verum end; end; definition let I be set ; let A be ManySortedSet of I; mode ManySortedRelation of A is ManySortedRelation of A,A; end; definition let I be set ; let A be ManySortedSet of I; let IT be ManySortedRelation of A; attrIT is MSEquivalence_Relation-like means :Def2: :: MSUALG_4:def 2 for i being set for R being Relation of (A . i) st i in I & IT . i = R holds R is Equivalence_Relation of (A . i); end; :: deftheorem Def2 defines MSEquivalence_Relation-like MSUALG_4:def_2_:_ for I being set for A being ManySortedSet of I for IT being ManySortedRelation of A holds ( IT is MSEquivalence_Relation-like iff for i being set for R being Relation of (A . i) st i in I & IT . i = R holds R is Equivalence_Relation of (A . i) ); definition let I be non empty set ; let A, B be ManySortedSet of I; let F be ManySortedRelation of A,B; let i be Element of I; :: original: . redefine funcF . i -> Relation of (A . i),(B . i); coherence F . i is Relation of (A . i),(B . i) by Def1; end; definition let S be non empty ManySortedSign ; let U1 be MSAlgebra over S; mode ManySortedRelation of U1 is ManySortedRelation of the Sorts of U1; end; definition let S be non empty ManySortedSign ; let U1 be MSAlgebra over S; let IT be ManySortedRelation of U1; attrIT is MSEquivalence-like means :Def3: :: MSUALG_4:def 3 IT is MSEquivalence_Relation-like ; end; :: deftheorem Def3 defines MSEquivalence-like MSUALG_4:def_3_:_ for S being non empty ManySortedSign for U1 being MSAlgebra over S for IT being ManySortedRelation of U1 holds ( IT is MSEquivalence-like iff IT is MSEquivalence_Relation-like ); registration let S be non empty non void ManySortedSign ; let U1 be MSAlgebra over S; cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like for ManySortedRelation of the Sorts of U1, the Sorts of U1; existence ex b1 being ManySortedRelation of U1 st b1 is MSEquivalence-like proof deffunc H1( Element of S) -> Element of K10(K11(( 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 Def1; reconsider f = f as ManySortedRelation of U1 ; take f ; ::_thesis: 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 Def2; hence f is MSEquivalence-like by Def3; ::_thesis: verum end; end; theorem Th1: :: MSUALG_4:1 for S being non empty non void ManySortedSign for U1 being MSAlgebra over S for s being SortSymbol of S for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S for s being SortSymbol of S for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s) let U1 be MSAlgebra over S; ::_thesis: for s being SortSymbol of S for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s) let s be SortSymbol of S; ::_thesis: for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s) let R be MSEquivalence-like ManySortedRelation of U1; ::_thesis: R . s is Equivalence_Relation of ( the Sorts of U1 . s) R is MSEquivalence_Relation-like by Def3; hence R . s is Equivalence_Relation of ( the Sorts of U1 . s) by Def2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let R be MSEquivalence-like ManySortedRelation of U1; attrR is MSCongruence-like means :Def4: :: MSUALG_4:def 4 for o being OperSymbol 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); end; :: deftheorem Def4 defines MSCongruence-like MSUALG_4:def_4_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for R being MSEquivalence-like ManySortedRelation of U1 holds ( R is MSCongruence-like iff for o being OperSymbol 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) ); registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like for ManySortedRelation of the Sorts of U1, the Sorts of U1; existence ex b1 being MSEquivalence-like ManySortedRelation of U1 st b1 is MSCongruence-like proof deffunc H1( Element of S) -> Element of K10(K11(( 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 Def1; 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 Def2; then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by Def3; take f ; ::_thesis: f is MSCongruence-like for o being OperSymbol 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 A2: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; then A3: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2; let o be OperSymbol 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) ) A4: dom x = dom (the_arity_of o) by MSUALG_3:6; assume A5: 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) A6: 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 A7: a in dom (the_arity_of o) ; ::_thesis: x . a = y . a then reconsider n = a as Nat by ORDINAL1:def_12; (the_arity_of o) . n in rng (the_arity_of o) by A7, FUNCT_1:def_3; then A8: 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 A7, PARTFUN1:def_6; then [(x . n),(y . n)] in f . ((the_arity_of o) . n) by A5, A4, A7; hence x . a = y . a by A8, RELAT_1:def_10; ::_thesis: verum end; set r = the_result_sort_of o; A9: f . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) by A1; A10: 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 A2, A3, 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 A4, A6, FUNCT_1:2; hence [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A9, A10, RELAT_1:def_10; ::_thesis: verum end; hence f is MSCongruence-like by Def4; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; mode MSCongruence of U1 is MSEquivalence-like MSCongruence-like ManySortedRelation of U1; end; definition let S be non empty non void ManySortedSign ; let U1 be MSAlgebra over S; let R be MSEquivalence-like ManySortedRelation of U1; let i be Element of S; :: original: . redefine funcR . i -> Equivalence_Relation of ( the Sorts of U1 . i); coherence R . i is Equivalence_Relation of ( the Sorts of U1 . i) by Th1; end; definition let S be non empty non void ManySortedSign ; let U1 be MSAlgebra over S; let R be MSEquivalence-like ManySortedRelation of U1; let i be Element of S; let x be Element of the Sorts of U1 . i; func Class (R,x) -> Subset of ( the Sorts of U1 . i) equals :: MSUALG_4:def 5 Class ((R . i),x); correctness coherence Class ((R . i),x) is Subset of ( the Sorts of U1 . i); ; end; :: deftheorem defines Class MSUALG_4:def_5_:_ for S being non empty non void ManySortedSign for U1 being MSAlgebra over S for R being MSEquivalence-like ManySortedRelation of U1 for i being Element of S for x being Element of the Sorts of U1 . i holds Class (R,x) = Class ((R . i),x); definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let R be MSCongruence of U1; func Class R -> V8() ManySortedSet of the carrier of S means :Def6: :: MSUALG_4:def 6 for s being Element of S holds it . s = Class (R . s); existence ex b1 being V8() ManySortedSet of the carrier of S st for s being Element of S holds b1 . s = Class (R . s) proof deffunc H1( Element of S) -> a_partition of the Sorts of U1 . \$1 = Class (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 i being set st i in the carrier of S holds not f . i is empty proof let i be set ; ::_thesis: ( i in the carrier of S implies not f . i is empty ) assume i in the carrier of S ; ::_thesis: not f . i is empty then reconsider s = i as Element of S ; consider x being set such that A2: x in the Sorts of U1 . s by XBOOLE_0:def_1; reconsider y = x as Element of the Sorts of U1 . s by A2; f . s = Class (R . s) by A1; then Class ((R . s),y) in f . s by EQREL_1:def_3; hence not f . i is empty ; ::_thesis: verum end; then reconsider f = f as V8() ManySortedSet of the carrier of S by PBOOLE:def_13; take f ; ::_thesis: for s being Element of S holds f . s = Class (R . s) thus for s being Element of S holds f . s = Class (R . s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being V8() ManySortedSet of the carrier of S st ( for s being Element of S holds b1 . s = Class (R . s) ) & ( for s being Element of S holds b2 . s = Class (R . s) ) holds b1 = b2 proof let C, D be V8() ManySortedSet of the carrier of S; ::_thesis: ( ( for s being Element of S holds C . s = Class (R . s) ) & ( for s being Element of S holds D . s = Class (R . s) ) implies C = D ) assume that A3: for s being Element of S holds C . s = Class (R . s) and A4: for s being Element of S holds D . s = Class (R . s) ; ::_thesis: C = D now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ C_._i_=_D_._i let i be set ; ::_thesis: ( i in the carrier of S implies C . i = D . i ) assume i in the carrier of S ; ::_thesis: C . i = D . i then reconsider s = i as Element of S ; C . s = Class (R . s) by A3; hence C . i = D . i by A4; ::_thesis: verum end; hence C = D by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def6 defines Class MSUALG_4:def_6_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for R being MSCongruence of U1 for b4 being V8() ManySortedSet of the carrier of S holds ( b4 = Class R iff for s being Element of S holds b4 . s = Class (R . s) ); begin definition let S be non empty non void ManySortedSign ; let M1, M2 be ManySortedSet of the carrier' of S; let F be ManySortedFunction of M1,M2; let o be OperSymbol of S; :: original: . redefine funcF . o -> Function of (M1 . o),(M2 . o); coherence F . o is Function of (M1 . o),(M2 . o) by PBOOLE:def_15; end; registration let I be non empty set ; let p be FinSequence of I; let X be ManySortedSet of I; clusterp * X -> dom p -defined for Function; coherence for b1 being Function st b1 = X * p holds b1 is dom p -defined proof rng p c= I ; then rng p c= dom X by PARTFUN1:def_2; then dom (X * p) = dom p by RELAT_1:27; then reconsider Xp = X * p as ManySortedSet of dom p by PARTFUN1:def_2, RELAT_1:def_18; Xp is ManySortedSet of dom p ; hence for b1 being Function st b1 = X * p holds b1 is dom p -defined ; ::_thesis: verum end; end; registration let I be non empty set ; let p be FinSequence of I; let X be ManySortedSet of I; clusterp * X -> dom p -defined total for dom p -defined Function; coherence for b1 being dom p -defined Function st b1 = X * p holds b1 is total proof rng p c= I ; then rng p c= dom X by PARTFUN1:def_2; then dom (X * p) = dom p by RELAT_1:27; then reconsider Xp = X * p as ManySortedSet of dom p by PARTFUN1:def_2; Xp is ManySortedSet of dom p ; hence for b1 being dom p -defined Function st b1 = X * p holds b1 is total ; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let o be OperSymbol of S; let A be non-empty MSAlgebra over S; let R be MSCongruence of A; let x be Element of Args (o,A); funcR # x -> Element of product ((Class R) * (the_arity_of o)) means :Def7: :: MSUALG_4:def 7 for n being Nat st n in dom (the_arity_of o) holds it . n = Class ((R . ((the_arity_of o) /. n)),(x . n)); existence ex b1 being Element of product ((Class R) * (the_arity_of o)) st for n being Nat st n in dom (the_arity_of o) holds b1 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) proof defpred S1[ set , set ] means for n being Nat st n = \$1 holds \$2 = Class ((R . ((the_arity_of o) /. n)),(x . n)); set ar = the_arity_of o; set da = dom (the_arity_of o); A1: for y being set st y in dom (the_arity_of o) holds ex u being set st S1[y,u] proof let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ex u being set st S1[y,u] ) assume y in dom (the_arity_of o) ; ::_thesis: ex u being set st S1[y,u] then reconsider n = y as Nat by ORDINAL1:def_12; take Class ((R . ((the_arity_of o) /. n)),(x . n)) ; ::_thesis: S1[y, Class ((R . ((the_arity_of o) /. n)),(x . n))] thus S1[y, Class ((R . ((the_arity_of o) /. n)),(x . n))] ; ::_thesis: verum end; consider f being Function such that A2: ( 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); A3: dom ((Class R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2; for y being set st y in dom ((Class R) * (the_arity_of o)) holds f . y in ((Class R) * (the_arity_of o)) . y proof let y be set ; ::_thesis: ( y in dom ((Class R) * (the_arity_of o)) implies f . y in ((Class R) * (the_arity_of o)) . y ) assume A4: y in dom ((Class R) * (the_arity_of o)) ; ::_thesis: f . y in ((Class R) * (the_arity_of o)) . y then reconsider n = y as Nat by ORDINAL1:def_12; (the_arity_of o) . y in rng (the_arity_of o) by A3, A4, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . y as Element of S ; A5: y in dom ( the Sorts of A * (the_arity_of o)) by A3, A4, PARTFUN1:def_2; then ( the Sorts of A * (the_arity_of o)) . y = the Sorts of A . ((the_arity_of o) . y) by FUNCT_1:12; then A6: x . y in the Sorts of A . s by A5, MSUALG_3:6; ( f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) & (the_arity_of o) /. n = (the_arity_of o) . n ) by A2, A3, A4, PARTFUN1:def_6; then A7: f . y in Class (R . s) by A6, EQREL_1:def_3; ((Class R) * (the_arity_of o)) . y = (Class R) . ((the_arity_of o) . y) by A4, FUNCT_1:12; hence f . y in ((Class R) * (the_arity_of o)) . y by A7, Def6; ::_thesis: verum end; then reconsider f = f as Element of product ((Class R) * (the_arity_of o)) by A2, A3, CARD_3:9; take f ; ::_thesis: for n being Nat st n in dom (the_arity_of o) holds f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) let n be Nat; ::_thesis: ( n in dom (the_arity_of o) implies f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) assume n in dom (the_arity_of o) ; ::_thesis: f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) hence f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Element of product ((Class R) * (the_arity_of o)) st ( for n being Nat st n in dom (the_arity_of o) holds b1 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) & ( for n being Nat st n in dom (the_arity_of o) holds b2 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) holds b1 = b2 proof let F, G be Element of product ((Class R) * (the_arity_of o)); ::_thesis: ( ( for n being Nat st n in dom (the_arity_of o) holds F . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) & ( for n being Nat st n in dom (the_arity_of o) holds G . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) implies F = G ) assume that A8: for n being Nat st n in dom (the_arity_of o) holds F . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) and A9: for n being Nat st n in dom (the_arity_of o) holds G . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ; ::_thesis: F = G A10: 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 A11: y in dom (the_arity_of o) ; ::_thesis: F . y = G . y then reconsider n = y as Nat by ORDINAL1:def_12; F . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) by A8, A11; hence F . y = G . y by A9, A11; ::_thesis: verum end; A12: 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 A12, A10, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def7 defines # MSUALG_4:def_7_:_ for S being non empty non void ManySortedSign for o being OperSymbol of S for A being non-empty MSAlgebra over S for R being MSCongruence of A for x being Element of Args (o,A) for b6 being Element of product ((Class R) * (the_arity_of o)) holds ( b6 = R # x iff for n being Nat st n in dom (the_arity_of o) holds b6 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ); definition let S be non empty non void ManySortedSign ; let o be OperSymbol of S; let A be non-empty MSAlgebra over S; let R be MSCongruence of A; func QuotRes (R,o) -> Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) means :Def8: :: MSUALG_4:def 8 for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = Class (R,x); existence ex b1 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (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)) -> Subset of ( the Sorts of A . (the_result_sort_of o)) = Class (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 (Class 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 (Class R) . (the_result_sort_of o) ) assume x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: f . x in (Class R) . (the_result_sort_of o) then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ; f . x1 = Class (R,x1) by A1; then f . x1 in Class (R . (the_result_sort_of o)) by EQREL_1:def_3; hence f . x in (Class R) . (the_result_sort_of o) by Def6; ::_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 ((Class R) * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2; then ((Class R) * the ResultSort of S) . o = (Class R) . ( the ResultSort of S . o) by A4, FUNCT_1:12 .= (Class 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),(((Class 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 = Class (R,x) thus for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = Class (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),(((Class R) * the ResultSort of S) . o); ::_thesis: ( ( for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = Class (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 = Class (R,x) and A6: for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = Class (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 = Class (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 QuotArgs (R,o) -> Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) means :: MSUALG_4:def 9 for x being Element of Args (o,A) holds it . x = R # x; existence ex b1 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st for x being Element of Args (o,A) holds b1 . x = R # x proof set ao = the_arity_of o; set D = Args (o,A); deffunc H1( Element of Args (o,A)) -> Element of product ((Class R) * (the_arity_of o)) = R # \$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 ((Class 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 ((Class R) #) . (the_arity_of o) ) assume x in ( the Sorts of A #) . (the_arity_of o) ; ::_thesis: f . x in ((Class R) #) . (the_arity_of o) then reconsider x1 = x as Element of Args (o,A) by A10, MSUALG_1:def_4; ( f . x1 = R # x1 & ((Class R) #) . (the_arity_of o) = product ((Class R) * (the_arity_of o)) ) by A8, FINSEQ_2:def_5; hence f . x in ((Class R) #) . (the_arity_of o) ; ::_thesis: verum end; o in dom (((Class R) #) * the Arity of S) by A9, PARTFUN1:def_2; then (((Class R) #) * the Arity of S) . o = ((Class R) #) . ( the Arity of S . o) by FUNCT_1:12 .= ((Class 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),((((Class 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 # x thus for x being Element of Args (o,A) holds f . x = R # x by A8; ::_thesis: verum end; uniqueness for b1, b2 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b1 . x = R # x ) & ( for x being Element of Args (o,A) holds b2 . x = R # 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),((((Class R) #) * the Arity of S) . o); ::_thesis: ( ( for x being Element of Args (o,A) holds f . x = R # x ) & ( for x being Element of Args (o,A) holds g . x = R # x ) implies f = g ) assume that A12: for x being Element of Args (o,A) holds f . x = R # x and A13: for x being Element of Args (o,A) holds g . x = R # 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 # 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 Def8 defines QuotRes MSUALG_4:def_8_:_ for S being non empty non void ManySortedSign for o being OperSymbol of S for A being non-empty MSAlgebra over S for R being MSCongruence of A for b5 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) holds ( b5 = QuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = Class (R,x) ); :: deftheorem defines QuotArgs MSUALG_4:def_9_:_ for S being non empty non void ManySortedSign for o being OperSymbol of S for A being non-empty MSAlgebra over S for R being MSCongruence of A for b5 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) holds ( b5 = QuotArgs (R,o) iff for x being Element of Args (o,A) holds b5 . x = R # x ); definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be MSCongruence of A; func QuotRes R -> ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S means :: MSUALG_4:def 10 for o being OperSymbol of S holds it . o = QuotRes (R,o); existence ex b1 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st for o being OperSymbol of S holds b1 . o = QuotRes (R,o) proof defpred S1[ set , set ] means for o being OperSymbol of S st o = \$1 holds \$2 = QuotRes (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 QuotRes (R,x1) ; ::_thesis: S1[x, QuotRes (R,x1)] thus S1[x, QuotRes (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 = QuotRes (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),(((Class 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),(((Class 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),(((Class R) * the ResultSort of S) . i) then reconsider i1 = i as OperSymbol of S ; f . i1 = QuotRes (R,i1) by A2; hence f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((Class R) * the ResultSort of S) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S by PBOOLE:def_15; take f ; ::_thesis: for o being OperSymbol of S holds f . o = QuotRes (R,o) thus for o being OperSymbol of S holds f . o = QuotRes (R,o) by A2; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = QuotRes (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotRes (R,o) ) holds b1 = b2 proof let f, g be ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = QuotRes (R,o) ) & ( for o being OperSymbol of S holds g . o = QuotRes (R,o) ) implies f = g ) assume that A3: for o being OperSymbol of S holds f . o = QuotRes (R,o) and A4: for o being OperSymbol of S holds g . o = QuotRes (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 = QuotRes (R,i1) by A3; hence f . i = g . i by A4; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; func QuotArgs R -> ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S means :: MSUALG_4:def 11 for o being OperSymbol of S holds it . o = QuotArgs (R,o); existence ex b1 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st for o being OperSymbol of S holds b1 . o = QuotArgs (R,o) proof defpred S1[ set , set ] means for o being OperSymbol of S st o = \$1 holds \$2 = QuotArgs (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 QuotArgs (R,x1) ; ::_thesis: S1[x, QuotArgs (R,x1)] thus S1[x, QuotArgs (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 = QuotArgs (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),((((Class 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),((((Class 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),((((Class R) #) * the Arity of S) . i) then reconsider i1 = i as OperSymbol of S ; f . i1 = QuotArgs (R,i1) by A6; hence f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((Class R) #) * the Arity of S) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S by PBOOLE:def_15; take f ; ::_thesis: for o being OperSymbol of S holds f . o = QuotArgs (R,o) thus for o being OperSymbol of S holds f . o = QuotArgs (R,o) by A6; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st ( for o being OperSymbol of S holds b1 . o = QuotArgs (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotArgs (R,o) ) holds b1 = b2 proof let f, g be ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = QuotArgs (R,o) ) & ( for o being OperSymbol of S holds g . o = QuotArgs (R,o) ) implies f = g ) assume that A7: for o being OperSymbol of S holds f . o = QuotArgs (R,o) and A8: for o being OperSymbol of S holds g . o = QuotArgs (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 = QuotArgs (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 QuotRes MSUALG_4:def_10_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being MSCongruence of A for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S holds ( b4 = QuotRes R iff for o being OperSymbol of S holds b4 . o = QuotRes (R,o) ); :: deftheorem defines QuotArgs MSUALG_4:def_11_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being MSCongruence of A for b4 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S holds ( b4 = QuotArgs R iff for o being OperSymbol of S holds b4 . o = QuotArgs (R,o) ); theorem Th2: :: MSUALG_4:2 for S being non empty non void ManySortedSign for o being OperSymbol of S for A being non-empty MSAlgebra over S for R being MSCongruence of A for x being set st x in (((Class R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R # a proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for A being non-empty MSAlgebra over S for R being MSCongruence of A for x being set st x in (((Class R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R # a let o be OperSymbol of S; ::_thesis: for A being non-empty MSAlgebra over S for R being MSCongruence of A for x being set st x in (((Class R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R # a let A be non-empty MSAlgebra over S; ::_thesis: for R being MSCongruence of A for x being set st x in (((Class R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R # a let R be MSCongruence of A; ::_thesis: for x being set st x in (((Class R) #) * the Arity of S) . o holds ex a being Element of Args (o,A) st x = R # a let x be set ; ::_thesis: ( x in (((Class R) #) * the Arity of S) . o implies ex a being Element of Args (o,A) st x = R # a ) assume A1: x in (((Class R) #) * the Arity of S) . o ; ::_thesis: ex a being Element of Args (o,A) st x = R # a set ar = the_arity_of o; A2: the_arity_of o = the Arity of S . o by MSUALG_1:def_1; then (((Class R) #) * the Arity of S) . o = product ((Class R) * (the_arity_of o)) by MSAFREE:1; then consider f being Function such that A3: f = x and A4: dom f = dom ((Class R) * (the_arity_of o)) and A5: for y being set st y in dom ((Class R) * (the_arity_of o)) holds f . y in ((Class R) * (the_arity_of o)) . y by A1, CARD_3:def_5; defpred S1[ set , set ] means \$2 in f . \$1; A6: dom ((Class 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 Class (R . ((the_arity_of o) /. n)) proof let n be Nat; ::_thesis: ( n in dom f implies f . n in Class (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 Class (R . ((the_arity_of o) /. n)) then (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, PARTFUN1:def_6; then ((Class R) * (the_arity_of o)) . n = (Class R) . s by A4, A8, FUNCT_1:12 .= Class (R . s) by Def6 ; hence f . n in Class (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, ORDINAL1:def_12; f . n in Class (R . s) by A7, A10; then consider a1 being set such that A11: ( a1 in the Sorts of A . s & f . n = Class ((R . s),a1) ) by EQREL_1:def_3; take a1 ; ::_thesis: S1[a,a1] thus S1[a,a1] by A11, 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 A16: ( g . y in f . y & f . y in ((Class R) * (the_arity_of o)) . y ) by A4, A5, A12, A13; reconsider n = y as Nat by A15, ORDINAL1:def_12; reconsider s = (the_arity_of o) /. n as Element of S ; A17: (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, A12, A13, A15, PARTFUN1:def_6; then ((Class R) * (the_arity_of o)) . y = (Class R) . s by A4, A12, A13, A15, FUNCT_1:12 .= Class (R . s) by Def6 ; then g . n in the Sorts of A . s by A16; hence g . y in ( the Sorts of A * (the_arity_of o)) . y by A15, A17, 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; A18: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_arity_of_o)_holds_ f_._x_=_(R_#_g)_._x let x be set ; ::_thesis: ( x in dom (the_arity_of o) implies f . x = (R # g) . x ) assume A19: x in dom (the_arity_of o) ; ::_thesis: f . x = (R # g) . x then reconsider n = x as Nat by ORDINAL1:def_12; reconsider s = (the_arity_of o) /. n as Element of S ; f . n in Class (R . s) by A4, A6, A7, A19; then consider a1 being set such that A20: a1 in the Sorts of A . s and A21: f . n = Class ((R . s),a1) by EQREL_1:def_3; g . n in f . n by A4, A6, A12, A19; then Class ((R . s),(g . n)) = Class ((R . s),a1) by A20, A21, EQREL_1:23; hence f . x = (R # g) . x by A19, A21, Def7; ::_thesis: verum end; take g ; ::_thesis: x = R # g dom (R # g) = dom ((Class R) * (the_arity_of o)) by CARD_3:9; hence x = R # g by A3, A4, A6, A18, FUNCT_1:2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let o be OperSymbol of S; let A be non-empty MSAlgebra over S; let R be MSCongruence of A; func QuotCharact (R,o) -> Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) means :Def12: :: MSUALG_4:def 12 for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds it . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a; existence ex b1 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a proof defpred S1[ set , set ] means for a being Element of Args (o,A) st \$1 = R # a holds \$2 = ((QuotRes (R,o)) * (Den (o,A))) . a; set Ca = (((Class R) #) * the Arity of S) . o; set Cr = ((Class R) * the ResultSort of S) . o; A1: for x being set st x in (((Class R) #) * the Arity of S) . o holds ex y being set st ( y in ((Class 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 (((Class R) #) * the Arity of S) . o implies ex y being set st ( y in ((Class R) * the ResultSort of S) . o & S1[x,y] ) ) assume x in (((Class R) #) * the Arity of S) . o ; ::_thesis: ex y being set st ( y in ((Class R) * the ResultSort of S) . o & S1[x,y] ) then consider a being Element of Args (o,A) such that A2: x = R # a by Th2; take y = ((QuotRes (R,o)) * (Den (o,A))) . a; ::_thesis: ( y in ((Class R) * the ResultSort of S) . o & S1[x,y] ) A3: o in the carrier' of S ; then o in dom ((Class R) * the ResultSort of S) by PARTFUN1:def_2; then A4: ((Class R) * the ResultSort of S) . o = (Class R) . ( the ResultSort of S . o) by FUNCT_1:12 .= (Class 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 (QuotRes (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 ((QuotRes (R,o)) * (Den (o,A))) = dom (Den (o,A)) ) by A6, FUNCT_2:def_1, RELAT_1:27; (QuotRes (R,o)) . ((Den (o,A)) . a) in rng (QuotRes (R,o)) by A6, FUNCT_1:def_3; then (QuotRes (R,o)) . ((Den (o,A)) . a) in (Class R) . (the_result_sort_of o) by A4; hence y in ((Class 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 # b implies y = ((QuotRes (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: ((QuotRes (R,o)) * (Den (o,A))) . b = (QuotRes (R,o)) . db by A7, FUNCT_1:12 .= Class (R,db) by Def8 .= Class ((R . (the_result_sort_of o)),db) ; assume A9: x = R # b ; ::_thesis: y = ((QuotRes (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 A11: n in dom a ; ::_thesis: [(a . n),(b . n)] in R . ((the_arity_of o) /. n) then A12: ( (R # a) . n = Class ((R . ((the_arity_of o) /. n)),(a . n)) & (R # b) . n = Class ((R . ((the_arity_of o) /. n)),(b . n)) ) by A10, Def7; 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 ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; then A14: a . n in ( the Sorts of A * (the_arity_of o)) . n by A11, A10, MSUALG_3:6; ( the Sorts of A * (the_arity_of o)) . n = the Sorts of A . ((the_arity_of o) . n) by A13, A11, A10, FUNCT_1:12 .= the Sorts of A . ((the_arity_of o) /. n) by A11, A10, PARTFUN1:def_6 ; hence [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, A14, A12, EQREL_1:35; ::_thesis: verum end; then A15: [da,db] in R . (the_result_sort_of o) by Def4; y = (QuotRes (R,o)) . ((Den (o,A)) . a) by A7, FUNCT_1:12 .= Class (R,da) by Def8 .= Class ((R . (the_result_sort_of o)),da) ; hence y = ((QuotRes (R,o)) * (Den (o,A))) . b by A8, A15, EQREL_1:35; ::_thesis: verum end; consider f being Function such that A16: ( dom f = (((Class R) #) * the Arity of S) . o & rng f c= ((Class R) * the ResultSort of S) . o & ( for x being set st x in (((Class R) #) * the Arity of S) . o holds S1[x,f . x] ) ) from FUNCT_1:sch_5(A1); reconsider f = f as Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) by A16, FUNCT_2:2; take f ; ::_thesis: for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds f . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a thus for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds f . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a by A16; ::_thesis: verum end; uniqueness for b1, b2 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds b2 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) holds b1 = b2 proof set ao = the_arity_of o; let F, G be Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o); ::_thesis: ( ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds F . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds G . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) implies F = G ) assume that A17: for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds F . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a and A18: for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds G . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ; ::_thesis: F = G A19: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then dom (((Class R) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2; then A20: (((Class R) #) * the Arity of S) . o = ((Class R) #) . ( the Arity of S . o) by A19, FUNCT_1:12 .= ((Class R) #) . (the_arity_of o) by MSUALG_1:def_1 ; A21: now__::_thesis:_for_x_being_set_st_x_in_((Class_R)_#)_._(the_arity_of_o)_holds_ F_._x_=_G_._x let x be set ; ::_thesis: ( x in ((Class R) #) . (the_arity_of o) implies F . x = G . x ) assume A22: x in ((Class R) #) . (the_arity_of o) ; ::_thesis: F . x = G . x then consider a being Element of Args (o,A) such that A23: x = R # a by A20, Th2; F . x = ((QuotRes (R,o)) * (Den (o,A))) . a by A17, A20, A22, A23; hence F . x = G . x by A18, A20, A22, A23; ::_thesis: verum end; ( dom F = ((Class R) #) . (the_arity_of o) & dom G = ((Class R) #) . (the_arity_of o) ) by A20, FUNCT_2:def_1; hence F = G by A21, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def12 defines QuotCharact MSUALG_4:def_12_:_ for S being non empty non void ManySortedSign for o being OperSymbol of S for A being non-empty MSAlgebra over S for R being MSCongruence of A for b5 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) holds ( b5 = QuotCharact (R,o) iff for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds b5 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ); definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be MSCongruence of A; func QuotCharact R -> ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S means :Def13: :: MSUALG_4:def 13 for o being OperSymbol of S holds it . o = QuotCharact (R,o); existence ex b1 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st for o being OperSymbol of S holds b1 . o = QuotCharact (R,o) proof defpred S1[ set , set ] means for o being OperSymbol of S st o = \$1 holds \$2 = QuotCharact (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 QuotCharact (R,x1) ; ::_thesis: S1[x, QuotCharact (R,x1)] thus S1[x, QuotCharact (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 = QuotCharact (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 ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i) proof let i be set ; ::_thesis: ( i in the carrier' of S implies f . i is Function of ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i) ) assume i in the carrier' of S ; ::_thesis: f . i is Function of ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i) then reconsider i1 = i as OperSymbol of S ; f . i1 = QuotCharact (R,i1) by A2; hence f . i is Function of ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S by PBOOLE:def_15; take f ; ::_thesis: for o being OperSymbol of S holds f . o = QuotCharact (R,o) thus for o being OperSymbol of S holds f . o = QuotCharact (R,o) by A2; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = QuotCharact (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotCharact (R,o) ) holds b1 = b2 proof let f, g be ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = QuotCharact (R,o) ) & ( for o being OperSymbol of S holds g . o = QuotCharact (R,o) ) implies f = g ) assume that A3: for o being OperSymbol of S holds f . o = QuotCharact (R,o) and A4: for o being OperSymbol of S holds g . o = QuotCharact (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 = QuotCharact (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 Def13 defines QuotCharact MSUALG_4:def_13_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being MSCongruence of A for b4 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S holds ( b4 = QuotCharact R iff for o being OperSymbol of S holds b4 . o = QuotCharact (R,o) ); definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let R be MSCongruence of U1; func QuotMSAlg (U1,R) -> MSAlgebra over S equals :: MSUALG_4:def 14 MSAlgebra(# (Class R),(QuotCharact R) #); coherence MSAlgebra(# (Class R),(QuotCharact R) #) is MSAlgebra over S ; end; :: deftheorem defines QuotMSAlg MSUALG_4:def_14_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for R being MSCongruence of U1 holds QuotMSAlg (U1,R) = MSAlgebra(# (Class R),(QuotCharact R) #); registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let R be MSCongruence of U1; cluster QuotMSAlg (U1,R) -> strict non-empty ; coherence ( QuotMSAlg (U1,R) is strict & QuotMSAlg (U1,R) is non-empty ) by MSUALG_1:def_3; end; definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let R be MSCongruence of U1; let s be SortSymbol of S; func MSNat_Hom (U1,R,s) -> Function of ( the Sorts of U1 . s),((Class R) . s) means :Def15: :: MSUALG_4:def 15 for x being set st x in the Sorts of U1 . s holds it . x = Class ((R . s),x); existence ex b1 being Function of ( the Sorts of U1 . s),((Class R) . s) st for x being set st x in the Sorts of U1 . s holds b1 . x = Class ((R . s),x) proof deffunc H1( set ) -> Element of K10(( the Sorts of U1 . s)) = Class ((R . s),\$1); consider f being Function such that A1: ( dom f = the Sorts of U1 . s & ( for x being set st x in the Sorts of U1 . s holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); for x being set st x in the Sorts of U1 . s holds f . x in (Class R) . s proof let x be set ; ::_thesis: ( x in the Sorts of U1 . s implies f . x in (Class R) . s ) assume A2: x in the Sorts of U1 . s ; ::_thesis: f . x in (Class R) . s then Class ((R . s),x) in Class (R . s) by EQREL_1:def_3; then f . x in Class (R . s) by A1, A2; hence f . x in (Class R) . s by Def6; ::_thesis: verum end; then reconsider f = f as Function of ( the Sorts of U1 . s),((Class R) . s) by A1, FUNCT_2:3; take f ; ::_thesis: for x being set st x in the Sorts of U1 . s holds f . x = Class ((R . s),x) thus for x being set st x in the Sorts of U1 . s holds f . x = Class ((R . s),x) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of ( the Sorts of U1 . s),((Class R) . s) st ( for x being set st x in the Sorts of U1 . s holds b1 . x = Class ((R . s),x) ) & ( for x being set st x in the Sorts of U1 . s holds b2 . x = Class ((R . s),x) ) holds b1 = b2 proof let f, g be Function of ( the Sorts of U1 . s),((Class R) . s); ::_thesis: ( ( for x being set st x in the Sorts of U1 . s holds f . x = Class ((R . s),x) ) & ( for x being set st x in the Sorts of U1 . s holds g . x = Class ((R . s),x) ) implies f = g ) assume that A3: for x being set st x in the Sorts of U1 . s holds f . x = Class ((R . s),x) and A4: for x being set st x in the Sorts of U1 . s holds g . x = Class ((R . s),x) ; ::_thesis: f = g A5: 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 A6: x in the Sorts of U1 . s ; ::_thesis: f . x = g . x then f . x = Class ((R . s),x) by A3; hence f . x = g . x by A4, A6; ::_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 A5, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def15 defines MSNat_Hom MSUALG_4:def_15_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for R being MSCongruence of U1 for s being SortSymbol of S for b5 being Function of ( the Sorts of U1 . s),((Class R) . s) holds ( b5 = MSNat_Hom (U1,R,s) iff for x being set st x in the Sorts of U1 . s holds b5 . x = Class ((R . s),x) ); definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let R be MSCongruence of U1; func MSNat_Hom (U1,R) -> ManySortedFunction of U1,(QuotMSAlg (U1,R)) means :Def16: :: MSUALG_4:def 16 for s being SortSymbol of S holds it . s = MSNat_Hom (U1,R,s); existence ex b1 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s) proof deffunc H1( Element of S) -> Function of ( the Sorts of U1 . \$1),((Class R) . \$1) = MSNat_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 = MSNat_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),((Class 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),((Class R) . i) ) assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of U1 . i),((Class R) . i) then reconsider s = i as Element of S ; f . s = MSNat_Hom (U1,R,s) by A1; hence f . i is Function of ( the Sorts of U1 . i),((Class R) . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Sorts of U1, Class R by PBOOLE:def_15; reconsider f = f as ManySortedFunction of U1,(QuotMSAlg (U1,R)) ; take f ; ::_thesis: for s being SortSymbol of S holds f . s = MSNat_Hom (U1,R,s) thus for s being SortSymbol of S holds f . s = MSNat_Hom (U1,R,s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st ( for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds b2 . s = MSNat_Hom (U1,R,s) ) holds b1 = b2 proof let F, G be ManySortedFunction of U1,(QuotMSAlg (U1,R)); ::_thesis: ( ( for s being SortSymbol of S holds F . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds G . s = MSNat_Hom (U1,R,s) ) implies F = G ) assume that A2: for s being SortSymbol of S holds F . s = MSNat_Hom (U1,R,s) and A3: for s being SortSymbol of S holds G . s = MSNat_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 = MSNat_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 Def16 defines MSNat_Hom MSUALG_4:def_16_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for R being MSCongruence of U1 for b4 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) holds ( b4 = MSNat_Hom (U1,R) iff for s being SortSymbol of S holds b4 . s = MSNat_Hom (U1,R,s) ); theorem :: MSUALG_4:3 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R) let U1 be non-empty MSAlgebra over S; ::_thesis: for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R) let R be MSCongruence of U1; ::_thesis: MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R) set F = MSNat_Hom (U1,R); set QA = QuotMSAlg (U1,R); set S1 = the Sorts of U1; for o being OperSymbol of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) proof let o be OperSymbol of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) ) assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) let x be Element of Args (o,U1); ::_thesis: ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_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: (((Class R) #) * the Arity of S) . o = product ((Class 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 ((MSNat_Hom (U1,R)) # x) . a = (R # x) . a proof let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies ((MSNat_Hom (U1,R)) # x) . a = (R # x) . a ) assume A4: a in dom (the_arity_of o) ; ::_thesis: ((MSNat_Hom (U1,R)) # x) . a = (R # x) . a then reconsider n = a as Nat by ORDINAL1:def_12; set Fo = MSNat_Hom (U1,R,((the_arity_of o) /. n)); set s = (the_arity_of o) /. n; A5: 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 A5, MSUALG_3:6; thus ((MSNat_Hom (U1,R)) # x) . a = ((MSNat_Hom (U1,R)) . ((the_arity_of o) /. n)) . (x . n) by A2, A4, MSUALG_3:def_6 .= (MSNat_Hom (U1,R,((the_arity_of o) /. n))) . xn by Def16 .= Class ((R . ((the_arity_of o) /. n)),(x . n)) by Def15 .= (R # x) . a by A4, Def7 ; ::_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 A6: ( 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 A6, MSUALG_1:def_5; then rng (Den (o,U1)) c= dom (QuotRes (R,o)) by A6, FUNCT_2:def_1; then A7: ( dom (Den (o,U1)) = Args (o,U1) & dom ((QuotRes (R,o)) * (Den (o,U1))) = dom (Den (o,U1)) ) by FUNCT_2:def_1, RELAT_1:27; dom (Class R) = the carrier of S by PARTFUN1:def_2; then ( dom (R # x) = dom ((Class R) * (the_arity_of o)) & rng (the_arity_of o) c= dom (Class R) ) by CARD_3:9; then ( dom ((MSNat_Hom (U1,R)) # x) = dom (the_arity_of o) & dom (R # x) = dom (the_arity_of o) ) by MSUALG_3:6, RELAT_1:27; then A8: (MSNat_Hom (U1,R)) # x = R # x by A3, FUNCT_1:2; Den (o,(QuotMSAlg (U1,R))) = (QuotCharact R) . o by MSUALG_1:def_6 .= QuotCharact (R,o) by Def13 ; then (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) = ((QuotRes (R,o)) * (Den (o,U1))) . x by A1, A8, Def12 .= (QuotRes (R,o)) . dx by A7, FUNCT_1:12 .= Class (R,dx) by Def8 .= (MSNat_Hom (U1,R,(the_result_sort_of o))) . dx by Def15 .= ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) by Def16 ; hence ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) ; ::_thesis: verum end; hence MSNat_Hom (U1,R) is_homomorphism U1, QuotMSAlg (U1,R) by MSUALG_3:def_7; :: according to MSUALG_3:def_8 ::_thesis: MSNat_Hom (U1,R) is "onto" for i being set st i in the carrier of S holds rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i ) assume i in the carrier of S ; ::_thesis: rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i then reconsider s = i as Element of S ; reconsider f = (MSNat_Hom (U1,R)) . i as Function of ( the Sorts of U1 . s),( the Sorts of (QuotMSAlg (U1,R)) . s) by PBOOLE:def_15; A9: dom f = the Sorts of U1 . s by FUNCT_2:def_1; A10: the Sorts of (QuotMSAlg (U1,R)) . s = Class (R . s) by Def6; for x being set st x in the Sorts of (QuotMSAlg (U1,R)) . i holds x in rng f proof let x be set ; ::_thesis: ( x in the Sorts of (QuotMSAlg (U1,R)) . i implies x in rng f ) A11: f = MSNat_Hom (U1,R,s) by Def16; assume x in the Sorts of (QuotMSAlg (U1,R)) . i ; ::_thesis: x in rng f then consider a1 being set such that A12: a1 in the Sorts of U1 . s and A13: x = Class ((R . s),a1) by A10, EQREL_1:def_3; f . a1 in rng f by A9, A12, FUNCT_1:def_3; hence x in rng f by A12, A13, A11, Def15; ::_thesis: verum end; then the Sorts of (QuotMSAlg (U1,R)) . i c= rng f by TARSKI:def_3; hence rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i by XBOOLE_0:def_10; ::_thesis: verum end; hence MSNat_Hom (U1,R) is "onto" by MSUALG_3:def_3; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; let s be SortSymbol of S; func MSCng (F,s) -> Equivalence_Relation of ( the Sorts of U1 . s) means :Def17: :: MSUALG_4:def 17 for x, y being Element of the Sorts of U1 . s holds ( [x,y] in it iff (F . s) . x = (F . s) . y ); existence ex b1 being Equivalence_Relation of ( the Sorts of U1 . s) st for x, y being Element of the Sorts of U1 . s holds ( [x,y] in b1 iff (F . s) . x = (F . s) . y ) proof defpred S1[ set , set ] means (F . s) . \$1 = (F . s) . \$2; set S1 = the Sorts of U1 . s; A1: for x, y being set st S1[x,y] holds S1[y,x] ; A2: for x, y, z being set st S1[x,y] & S1[y,z] holds S1[x,z] ; A3: for x being set st x in the Sorts of U1 . s holds S1[x,x] ; consider R being Equivalence_Relation of ( the Sorts of U1 . s) such that A4: for x, y being set holds ( [x,y] in R iff ( x in the Sorts of U1 . s & y in the Sorts of U1 . s & S1[x,y] ) ) from EQREL_1:sch_1(A3, A1, A2); take R ; ::_thesis: for x, y being Element of the Sorts of U1 . s holds ( [x,y] in R iff (F . s) . x = (F . s) . y ) let x, y be Element of the Sorts of U1 . s; ::_thesis: ( [x,y] in R iff (F . s) . x = (F . s) . y ) thus ( [x,y] in R iff (F . s) . x = (F . s) . y ) by A4; ::_thesis: verum end; uniqueness for b1, b2 being Equivalence_Relation of ( the Sorts of U1 . s) st ( for x, y being Element of the Sorts of U1 . s holds ( [x,y] in b1 iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds ( [x,y] in b2 iff (F . s) . x = (F . s) . y ) ) holds b1 = b2 proof let R, S be Equivalence_Relation of ( the Sorts of U1 . s); ::_thesis: ( ( for x, y being Element of the Sorts of U1 . s holds ( [x,y] in R iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds ( [x,y] in S iff (F . s) . x = (F . s) . y ) ) implies R = S ) assume that A5: for x, y being Element of the Sorts of U1 . s holds ( [x,y] in R iff (F . s) . x = (F . s) . y ) and A6: for x, y being Element of the Sorts of U1 . s holds ( [x,y] in S iff (F . s) . x = (F . s) . y ) ; ::_thesis: R = S now__::_thesis:_for_x,_y_being_set_holds_ (_(_[x,y]_in_R_implies_[x,y]_in_S_)_&_(_[x,y]_in_S_implies_[x,y]_in_R_)_) let x, y be set ; ::_thesis: ( ( [x,y] in R implies [x,y] in S ) & ( [x,y] in S implies [x,y] in R ) ) thus ( [x,y] in R implies [x,y] in S ) ::_thesis: ( [x,y] in S implies [x,y] in R ) proof assume A7: [x,y] in R ; ::_thesis: [x,y] in S then reconsider a = x, b = y as Element of the Sorts of U1 . s by ZFMISC_1:87; (F . s) . a = (F . s) . b by A5, A7; hence [x,y] in S by A6; ::_thesis: verum end; assume A8: [x,y] in S ; ::_thesis: [x,y] in R then reconsider a = x, b = y as Element of the Sorts of U1 . s by ZFMISC_1:87; (F . s) . a = (F . s) . b by A6, A8; hence [x,y] in R by A5; ::_thesis: verum end; hence R = S by RELAT_1:def_2; ::_thesis: verum end; end; :: deftheorem Def17 defines MSCng MSUALG_4:def_17_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for s being SortSymbol of S for b6 being Equivalence_Relation of ( the Sorts of U1 . s) holds ( b6 = MSCng (F,s) iff for x, y being Element of the Sorts of U1 . s holds ( [x,y] in b6 iff (F . s) . x = (F . s) . y ) ); definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; assume A1: F is_homomorphism U1,U2 ; func MSCng F -> MSCongruence of U1 means :Def18: :: MSUALG_4:def 18 for s being SortSymbol of S holds it . s = MSCng (F,s); existence ex b1 being MSCongruence of U1 st for s being SortSymbol of S holds b1 . s = MSCng (F,s) proof deffunc H1( Element of S) -> Equivalence_Relation of ( the Sorts of U1 . \$1) = MSCng (F,\$1); consider f being Function such that A2: ( 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 A2, 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 reconsider s = i as Element of S ; f . i = MSCng (F,s) by A2; 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 by Def1; 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 that A3: i in the carrier of S and A4: f . i = R ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i) reconsider s = i as Element of S by A3; R = MSCng (F,s) by A2, A4; hence R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum end; then f is MSEquivalence_Relation-like by Def2; then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by Def3; for o being OperSymbol 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 OperSymbol 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) ) set ao = the_arity_of o; set ro = the_result_sort_of o; set S1 = the Sorts of U1; A5: dom x = dom (the_arity_of o) by MSUALG_3:6; A6: dom y = 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: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_ (F_#_x)_._n_=_(F_#_y)_._n let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies (F # x) . n = (F # y) . n ) assume A9: n in dom (the_arity_of o) ; ::_thesis: (F # x) . n = (F # y) . n then reconsider m = n as Nat by ORDINAL1:def_12; A10: ( (F # x) . m = (F . ((the_arity_of o) /. m)) . (x . m) & (F # y) . m = (F . ((the_arity_of o) /. m)) . (y . m) ) by A5, A6, A9, MSUALG_3:def_6; (the_arity_of o) . m in rng (the_arity_of o) by A9, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . m as SortSymbol of S ; A11: n in dom ( the Sorts of U1 * (the_arity_of o)) by A9, PARTFUN1:def_2; then ( x . m in ( the Sorts of U1 * (the_arity_of o)) . n & y . m in ( the Sorts of U1 * (the_arity_of o)) . n ) by MSUALG_3:6; then reconsider x1 = x . m, y1 = y . m as Element of the Sorts of U1 . s by A11, FUNCT_1:12; A12: [x1,y1] in f . ((the_arity_of o) /. m) by A7, A5, A9; A13: (the_arity_of o) /. m = (the_arity_of o) . m by A9, PARTFUN1:def_6; then f . ((the_arity_of o) /. m) = MSCng (F,s) by A2; hence (F # x) . n = (F # y) . n by A10, A13, A12, Def17; ::_thesis: verum end; ( dom (F # x) = dom (the_arity_of o) & dom (F # y) = dom (the_arity_of o) ) by MSUALG_3:6; then A14: F # x = F # y by A8, FUNCT_1:2; reconsider ro = the_result_sort_of o as SortSymbol of S ; A15: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; then A16: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2; 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 A15, A16, FUNCT_1:12 .= the Sorts of U1 . ro by MSUALG_1:def_2 ; then reconsider Dx = (Den (o,U1)) . x, Dy = (Den (o,U1)) . y as Element of the Sorts of U1 . ro ; A17: (F . ro) . Dy = (Den (o,U2)) . (F # y) by A1, MSUALG_3:def_7; ( f . ro = MSCng (F,ro) & (F . ro) . Dx = (Den (o,U2)) . (F # x) ) by A1, A2, MSUALG_3:def_7; hence [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A14, A17, Def17; ::_thesis: verum end; then reconsider f = f as MSCongruence of U1 by Def4; take f ; ::_thesis: for s being SortSymbol of S holds f . s = MSCng (F,s) thus for s being SortSymbol of S holds f . s = MSCng (F,s) by A2; ::_thesis: verum end; uniqueness for b1, b2 being MSCongruence of U1 st ( for s being SortSymbol of S holds b1 . s = MSCng (F,s) ) & ( for s being SortSymbol of S holds b2 . s = MSCng (F,s) ) holds b1 = b2 proof let C1, C2 be MSCongruence of U1; ::_thesis: ( ( for s being SortSymbol of S holds C1 . s = MSCng (F,s) ) & ( for s being SortSymbol of S holds C2 . s = MSCng (F,s) ) implies C1 = C2 ) assume that A18: for s being SortSymbol of S holds C1 . s = MSCng (F,s) and A19: for s being SortSymbol of S holds C2 . s = MSCng (F,s) ; ::_thesis: C1 = C2 now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ C1_._i_=_C2_._i let i be set ; ::_thesis: ( i in the carrier of S implies C1 . i = C2 . i ) assume i in the carrier of S ; ::_thesis: C1 . i = C2 . i then reconsider s = i as Element of S ; C1 . s = MSCng (F,s) by A18; hence C1 . i = C2 . i by A19; ::_thesis: verum end; hence C1 = C2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def18 defines MSCng MSUALG_4:def_18_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds for b5 being MSCongruence of U1 holds ( b5 = MSCng F iff for s being SortSymbol of S holds b5 . s = MSCng (F,s) ); definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; let s be SortSymbol of S; assume A1: F is_homomorphism U1,U2 ; func MSHomQuot (F,s) -> Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) means :Def19: :: MSUALG_4:def 19 for x being Element of the Sorts of U1 . s holds it . (Class ((MSCng (F,s)),x)) = (F . s) . x; existence ex b1 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x proof set qa = QuotMSAlg (U1,(MSCng F)); set cqa = the Sorts of (QuotMSAlg (U1,(MSCng 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 = Class ((MSCng (F,s)),a) holds \$2 = (F . s) . a; A2: the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) by Def6 .= Class (MSCng (F,s)) by A1, Def18 ; A3: for x being set st x in the Sorts of (QuotMSAlg (U1,(MSCng 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 (QuotMSAlg (U1,(MSCng F))) . s implies ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) ) assume A4: x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s ; ::_thesis: ex y being set st ( y in the Sorts of U2 . s & S1[x,y] ) then reconsider x1 = x as Subset of ( the Sorts of U1 . s) by A2; consider a being set such that A5: a in the Sorts of U1 . s and A6: x1 = Class ((MSCng (F,s)),a) by A2, A4, EQREL_1:def_3; 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 = Class ((MSCng (F,s)),b) implies y = (F . s) . b ) assume x = Class ((MSCng (F,s)),b) ; ::_thesis: y = (F . s) . b then b in Class ((MSCng (F,s)),a) by A6, EQREL_1:23; then [b,a] in MSCng (F,s) by EQREL_1:19; hence y = (F . s) . b by Def17; ::_thesis: verum end; consider G being Function such that A7: ( dom G = the Sorts of (QuotMSAlg (U1,(MSCng F))) . s & rng G c= the Sorts of U2 . s & ( for x being set st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds S1[x,G . x] ) ) from FUNCT_1:sch_5(A3); reconsider G = G as Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) by A7, FUNCT_2:def_1, RELSET_1:4; take G ; ::_thesis: for x being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),x)) = (F . s) . x let a be Element of the Sorts of U1 . s; ::_thesis: G . (Class ((MSCng (F,s)),a)) = (F . s) . a Class ((MSCng (F,s)),a) in Class (MSCng (F,s)) by EQREL_1:def_3; hence G . (Class ((MSCng (F,s)),a)) = (F . s) . a by A2, A7; ::_thesis: verum end; uniqueness for b1, b2 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) holds b1 = b2 proof set qa = QuotMSAlg (U1,(MSCng F)); set cqa = the Sorts of (QuotMSAlg (U1,(MSCng F))); set u1 = the Sorts of U1; set u2 = the Sorts of U2; let H, G be Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),x)) = (F . s) . x ) implies H = G ) assume that A8: for a being Element of the Sorts of U1 . s holds H . (Class ((MSCng (F,s)),a)) = (F . s) . a and A9: for a being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),a)) = (F . s) . a ; ::_thesis: H = G A10: the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) by Def6 .= Class (MSCng (F,s)) by A1, Def18 ; for x being set st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds H . x = G . x proof let x be set ; ::_thesis: ( x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s implies H . x = G . x ) assume A11: x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s ; ::_thesis: H . x = G . x then reconsider x1 = x as Subset of ( the Sorts of U1 . s) by A10; consider a being set such that A12: a in the Sorts of U1 . s and A13: x1 = Class ((MSCng (F,s)),a) by A10, A11, EQREL_1:def_3; reconsider a = a as Element of the Sorts of U1 . s by A12; thus H . x = (F . s) . a by A8, A13 .= G . x by A9, A13 ; ::_thesis: verum end; hence H = G by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def19 defines MSHomQuot MSUALG_4:def_19_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for s being SortSymbol of S st F is_homomorphism U1,U2 holds for b6 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) holds ( b6 = MSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b6 . (Class ((MSCng (F,s)),x)) = (F . s) . x ); definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; func MSHomQuot F -> ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 means :Def20: :: MSUALG_4:def 20 for s being SortSymbol of S holds it . s = MSHomQuot (F,s); existence ex b1 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s) proof deffunc H1( Element of S) -> Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . \$1),( the Sorts of U2 . \$1) = MSHomQuot (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 = MSHomQuot (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 (QuotMSAlg (U1,(MSCng 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 (QuotMSAlg (U1,(MSCng F))) . i),( the Sorts of U2 . i) ) assume i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . i),( the Sorts of U2 . i) then reconsider s = i as Element of S ; f . s = MSHomQuot (F,s) by A1; hence f . i is Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . i),( the Sorts of U2 . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of the Sorts of (QuotMSAlg (U1,(MSCng F))), the Sorts of U2 by PBOOLE:def_15; reconsider f = f as ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 ; take f ; ::_thesis: for s being SortSymbol of S holds f . s = MSHomQuot (F,s) thus for s being SortSymbol of S holds f . s = MSHomQuot (F,s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st ( for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds b2 . s = MSHomQuot (F,s) ) holds b1 = b2 proof let H, G be ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2; ::_thesis: ( ( for s being SortSymbol of S holds H . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds G . s = MSHomQuot (F,s) ) implies H = G ) assume that A2: for s being SortSymbol of S holds H . s = MSHomQuot (F,s) and A3: for s being SortSymbol of S holds G . s = MSHomQuot (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 = MSHomQuot (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 Def20 defines MSHomQuot MSUALG_4:def_20_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for b5 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 holds ( b5 = MSHomQuot F iff for s being SortSymbol of S holds b5 . s = MSHomQuot (F,s) ); theorem Th4: :: MSUALG_4:4 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 ) set mc = MSCng F; set qa = QuotMSAlg (U1,(MSCng F)); set qh = MSHomQuot F; set S1 = the Sorts of U1; assume A1: F is_homomorphism U1,U2 ; ::_thesis: MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 for o being OperSymbol of S st Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} holds for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) proof let o be OperSymbol of S; ::_thesis: ( Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} implies for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) ) assume Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} ; ::_thesis: for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) let x be Element of Args (o,(QuotMSAlg (U1,(MSCng F)))); ::_thesis: ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) set ro = the_result_sort_of o; set ar = the_arity_of o; A2: dom x = dom (the_arity_of o) by MSUALG_3:6; Args (o,(QuotMSAlg (U1,(MSCng F)))) = (((Class (MSCng F)) #) * the Arity of S) . o by MSUALG_1:def_4; then consider a being Element of Args (o,U1) such that A3: x = (MSCng F) # a by Th2; A4: dom a = dom (the_arity_of o) by MSUALG_3:6; A5: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_ ((MSHomQuot_F)_#_x)_._y_=_(F_#_a)_._y let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((MSHomQuot F) # x) . y = (F # a) . y ) assume A6: y in dom (the_arity_of o) ; ::_thesis: ((MSHomQuot F) # x) . y = (F # a) . y then reconsider n = y as Nat by ORDINAL1:def_12; (the_arity_of o) . n in rng (the_arity_of o) by A6, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . n as SortSymbol of S ; A7: (the_arity_of o) /. n = (the_arity_of o) . n by A6, PARTFUN1:def_6; then x . n = Class (((MSCng F) . s),(a . n)) by A3, A6, Def7; then A8: x . n = Class ((MSCng (F,s)),(a . n)) by A1, Def18; A9: n in dom ( the Sorts of U1 * (the_arity_of o)) by A6, PARTFUN1:def_2; then a . n in ( the Sorts of U1 * (the_arity_of o)) . n by MSUALG_3:6; then reconsider an = a . n as Element of the Sorts of U1 . s by A9, FUNCT_1:12; ((MSHomQuot F) # x) . n = ((MSHomQuot F) . s) . (x . n) by A2, A6, A7, MSUALG_3:def_6 .= (MSHomQuot (F,s)) . (x . n) by Def20 .= (F . s) . an by A1, A8, Def19 .= (F # a) . n by A4, A6, A7, MSUALG_3:def_6 ; hence ((MSHomQuot 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 A10: ( 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 (QuotRes ((MSCng F),o)) by A10, FUNCT_2:def_1; then A11: ( dom (Den (o,U1)) = Args (o,U1) & dom ((QuotRes ((MSCng 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 A12: product ((Class (MSCng F)) * (the_arity_of o)) = (((Class (MSCng 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 A10, MSUALG_1:def_5; A13: (MSHomQuot F) . (the_result_sort_of o) = MSHomQuot (F,(the_result_sort_of o)) by Def20; Den (o,(QuotMSAlg (U1,(MSCng F)))) = (QuotCharact (MSCng F)) . o by MSUALG_1:def_6 .= QuotCharact ((MSCng F),o) by Def13 ; then (Den (o,(QuotMSAlg (U1,(MSCng F))))) . x = ((QuotRes ((MSCng F),o)) * (Den (o,U1))) . a by A3, A12, Def12 .= (QuotRes ((MSCng F),o)) . da by A11, FUNCT_1:12 .= Class ((MSCng F),da) by Def8 .= Class ((MSCng (F,(the_result_sort_of o))),da) by A1, Def18 ; then A14: ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (F . (the_result_sort_of o)) . ((Den (o,U1)) . a) by A1, A13, Def19 .= (Den (o,U2)) . (F # a) by A1, MSUALG_3:def_7 ; ( dom ((MSHomQuot F) # x) = dom (the_arity_of o) & dom (F # a) = dom (the_arity_of o) ) by MSUALG_3:6; hence ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) by A5, A14, FUNCT_1:2; ::_thesis: verum end; hence MSHomQuot F is_homomorphism QuotMSAlg (U1,(MSCng F)),U2 by MSUALG_3:def_7; :: according to MSUALG_3:def_9 ::_thesis: MSHomQuot F is "1-1" for i being set st i in the carrier of S holds (MSHomQuot F) . i is one-to-one proof let i be set ; ::_thesis: ( i in the carrier of S implies (MSHomQuot F) . i is one-to-one ) set f = (MSHomQuot F) . i; assume i in the carrier of S ; ::_thesis: (MSHomQuot F) . i is one-to-one then reconsider s = i as SortSymbol of S ; A15: (MSHomQuot F) . i = MSHomQuot (F,s) by Def20; for x1, x2 being set st x1 in dom ((MSHomQuot F) . i) & x2 in dom ((MSHomQuot F) . i) & ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom ((MSHomQuot F) . i) & x2 in dom ((MSHomQuot F) . i) & ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 implies x1 = x2 ) assume that A16: x1 in dom ((MSHomQuot F) . i) and A17: x2 in dom ((MSHomQuot F) . i) and A18: ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 ; ::_thesis: x1 = x2 x1 in (Class (MSCng F)) . s by A15, A16, FUNCT_2:def_1; then x1 in Class ((MSCng F) . s) by Def6; then consider a1 being set such that A19: a1 in the Sorts of U1 . s and A20: x1 = Class (((MSCng F) . s),a1) by EQREL_1:def_3; x2 in (Class (MSCng F)) . s by A15, A17, FUNCT_2:def_1; then x2 in Class ((MSCng F) . s) by Def6; then consider a2 being set such that A21: a2 in the Sorts of U1 . s and A22: x2 = Class (((MSCng F) . s),a2) by EQREL_1:def_3; reconsider a2 = a2 as Element of the Sorts of U1 . s by A21; A23: (MSCng F) . s = MSCng (F,s) by A1, Def18; then A24: ((MSHomQuot F) . i) . x2 = (F . s) . a2 by A1, A15, A22, Def19; reconsider a1 = a1 as Element of the Sorts of U1 . s by A19; ((MSHomQuot F) . i) . x1 = (F . s) . a1 by A1, A15, A23, A20, Def19; then [a1,a2] in MSCng (F,s) by A18, A24, Def17; hence x1 = x2 by A23, A20, A22, EQREL_1:35; ::_thesis: verum end; hence (MSHomQuot F) . i is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; hence MSHomQuot F is "1-1" by MSUALG_3:1; ::_thesis: verum end; theorem Th5: :: MSUALG_4:5 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 implies MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 ) set mc = MSCng F; set qa = QuotMSAlg (U1,(MSCng F)); set qh = MSHomQuot F; set Sq = the Sorts of (QuotMSAlg (U1,(MSCng F))); set S1 = the Sorts of U1; set S2 = the Sorts of U2; assume A1: F is_epimorphism U1,U2 ; ::_thesis: MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 then A2: F is_homomorphism U1,U2 by MSUALG_3:def_8; A3: F is "onto" by A1, MSUALG_3:def_8; for i being set st i in the carrier of S holds rng ((MSHomQuot F) . i) = the Sorts of U2 . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng ((MSHomQuot F) . i) = the Sorts of U2 . i ) set f = (MSHomQuot F) . i; assume i in the carrier of S ; ::_thesis: rng ((MSHomQuot F) . i) = the Sorts of U2 . i then reconsider s = i as SortSymbol of S ; A4: rng (F . s) = the Sorts of U2 . s by A3, MSUALG_3:def_3; A5: (MSHomQuot F) . i = MSHomQuot (F,s) by Def20; hence rng ((MSHomQuot F) . i) c= the Sorts of U2 . i by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of U2 . i c= rng ((MSHomQuot F) . i) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of U2 . i or x in rng ((MSHomQuot F) . i) ) assume x in the Sorts of U2 . i ; ::_thesis: x in rng ((MSHomQuot F) . i) then consider a being set such that A6: a in dom (F . s) and A7: (F . s) . a = x by A4, FUNCT_1:def_3; A8: ( MSCng (F,s) = (MSCng F) . s & the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) ) by A2, Def6, Def18; reconsider a = a as Element of the Sorts of U1 . s by A6; dom ((MSHomQuot F) . i) = the Sorts of (QuotMSAlg (U1,(MSCng F))) . s by A5, FUNCT_2:def_1; then A9: Class ((MSCng (F,s)),a) in dom ((MSHomQuot F) . i) by A8, EQREL_1:def_3; ((MSHomQuot F) . i) . (Class ((MSCng (F,s)),a)) = x by A2, A5, A7, Def19; hence x in rng ((MSHomQuot F) . i) by A9, FUNCT_1:def_3; ::_thesis: verum end; then A10: MSHomQuot F is "onto" by MSUALG_3:def_3; MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 by A2, Th4; then ( MSHomQuot F is_homomorphism QuotMSAlg (U1,(MSCng F)),U2 & MSHomQuot F is "1-1" ) by MSUALG_3:def_9; hence MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 by A10, MSUALG_3:13; ::_thesis: verum end; theorem :: MSUALG_4:6 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 implies QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic ) assume F is_epimorphism U1,U2 ; ::_thesis: QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic then MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 by Th5; hence QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic by MSUALG_3:def_11; ::_thesis: verum end;