:: ENDALG semantic presentation begin definition let UA be Universal_Algebra; func UAEnd UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA means :Def1: :: ENDALG:def 1 for h being Function of UA,UA holds ( h in it iff h is_homomorphism UA,UA ); existence ex b1 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st for h being Function of UA,UA holds ( h in b1 iff h is_homomorphism UA,UA ) proof set F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } ; A1: id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } proof set I = id the carrier of UA; ( id the carrier of UA in Funcs ( the carrier of UA, the carrier of UA) & id the carrier of UA is_homomorphism UA,UA ) by ALG_1:5, FUNCT_2:8; hence id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } ; ::_thesis: verum end; { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } is functional proof let q be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not q in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } or q is set ) assume q in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } ; ::_thesis: q is set then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st ( q = x & x is_homomorphism UA,UA ) ; hence q is set ; ::_thesis: verum end; then reconsider F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } as functional non empty set by A1; F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA proof let a be Element of F; :: according to FUNCT_2:def_12 ::_thesis: a is Element of bool [: the carrier of UA, the carrier of UA:] a in F ; then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st ( a = x & x is_homomorphism UA,UA ) ; hence a is Element of bool [: the carrier of UA, the carrier of UA:] ; ::_thesis: verum end; then reconsider F = F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA ; take F ; ::_thesis: for h being Function of UA,UA holds ( h in F iff h is_homomorphism UA,UA ) let h be Function of UA,UA; ::_thesis: ( h in F iff h is_homomorphism UA,UA ) thus ( h in F implies h is_homomorphism UA,UA ) ::_thesis: ( h is_homomorphism UA,UA implies h in F ) proof assume h in F ; ::_thesis: h is_homomorphism UA,UA then ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st ( f = h & f is_homomorphism UA,UA ) ; hence h is_homomorphism UA,UA ; ::_thesis: verum end; A2: h is Element of Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:8; assume h is_homomorphism UA,UA ; ::_thesis: h in F hence h in F by A2; ::_thesis: verum end; uniqueness for b1, b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA st ( for h being Function of UA,UA holds ( h in b1 iff h is_homomorphism UA,UA ) ) & ( for h being Function of UA,UA holds ( h in b2 iff h is_homomorphism UA,UA ) ) holds b1 = b2 proof let F1, F2 be FUNCTION_DOMAIN of the carrier of UA, the carrier of UA; ::_thesis: ( ( for h being Function of UA,UA holds ( h in F1 iff h is_homomorphism UA,UA ) ) & ( for h being Function of UA,UA holds ( h in F2 iff h is_homomorphism UA,UA ) ) implies F1 = F2 ) assume that A3: for h being Function of UA,UA holds ( h in F1 iff h is_homomorphism UA,UA ) and A4: for h being Function of UA,UA holds ( h in F2 iff h is_homomorphism UA,UA ) ; ::_thesis: F1 = F2 A5: for f being Element of F2 holds f is Function of UA,UA ; A6: F2 c= F1 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 ) assume A7: q in F2 ; ::_thesis: q in F1 then reconsider h1 = q as Function of UA,UA by A5; h1 is_homomorphism UA,UA by A4, A7; hence q in F1 by A3; ::_thesis: verum end; A8: for f being Element of F1 holds f is Function of UA,UA ; F1 c= F2 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 ) assume A9: q in F1 ; ::_thesis: q in F2 then reconsider h1 = q as Function of UA,UA by A8; h1 is_homomorphism UA,UA by A3, A9; hence q in F2 by A4; ::_thesis: verum end; hence F1 = F2 by A6, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def1 defines UAEnd ENDALG:def_1_:_ for UA being Universal_Algebra for b2 being FUNCTION_DOMAIN of the carrier of UA, the carrier of UA holds ( b2 = UAEnd UA iff for h being Function of UA,UA holds ( h in b2 iff h is_homomorphism UA,UA ) ); theorem :: ENDALG:1 for UA being Universal_Algebra holds UAEnd UA c= Funcs ( the carrier of UA, the carrier of UA) proof let UA be Universal_Algebra; ::_thesis: UAEnd UA c= Funcs ( the carrier of UA, the carrier of UA) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in UAEnd UA or q in Funcs ( the carrier of UA, the carrier of UA) ) assume q in UAEnd UA ; ::_thesis: q in Funcs ( the carrier of UA, the carrier of UA) then q is Element of UAEnd UA ; hence q in Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:9; ::_thesis: verum end; theorem Th2: :: ENDALG:2 for UA being Universal_Algebra holds id the carrier of UA in UAEnd UA proof let UA be Universal_Algebra; ::_thesis: id the carrier of UA in UAEnd UA id the carrier of UA is_homomorphism UA,UA by ALG_1:5; hence id the carrier of UA in UAEnd UA by Def1; ::_thesis: verum end; theorem Th3: :: ENDALG:3 for UA being Universal_Algebra for f1, f2 being Element of UAEnd UA holds f1 * f2 in UAEnd UA proof let UA be Universal_Algebra; ::_thesis: for f1, f2 being Element of UAEnd UA holds f1 * f2 in UAEnd UA let f1, f2 be Element of UAEnd UA; ::_thesis: f1 * f2 in UAEnd UA ( f1 is_homomorphism UA,UA & f2 is_homomorphism UA,UA ) by Def1; then f1 * f2 is_homomorphism UA,UA by ALG_1:6; hence f1 * f2 in UAEnd UA by Def1; ::_thesis: verum end; definition let UA be Universal_Algebra; func UAEndComp UA -> BinOp of (UAEnd UA) means :Def2: :: ENDALG:def 2 for x, y being Element of UAEnd UA holds it . (x,y) = y * x; existence ex b1 being BinOp of (UAEnd UA) st for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x proof defpred S1[ Element of UAEnd UA, Element of UAEnd UA, set ] means \$3 = \$2 * \$1; A1: for x, y being Element of UAEnd UA ex m being Element of UAEnd UA st S1[x,y,m] proof let x, y be Element of UAEnd UA; ::_thesis: ex m being Element of UAEnd UA st S1[x,y,m] reconsider xx = x, yy = y as Function of UA,UA ; reconsider m = yy * xx as Element of UAEnd UA by Th3; take m ; ::_thesis: S1[x,y,m] thus S1[x,y,m] ; ::_thesis: verum end; ex B being BinOp of (UAEnd UA) st for x, y being Element of UAEnd UA holds S1[x,y,B . (x,y)] from BINOP_1:sch_3(A1); hence ex b1 being BinOp of (UAEnd UA) st for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (UAEnd UA) st ( for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ) holds b1 = b2 proof let b1, b2 be BinOp of (UAEnd UA); ::_thesis: ( ( for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x ) & ( for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ) implies b1 = b2 ) assume that A2: for x, y being Element of UAEnd UA holds b1 . (x,y) = y * x and A3: for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ; ::_thesis: b1 = b2 for x, y being Element of UAEnd UA holds b1 . (x,y) = b2 . (x,y) proof let x, y be Element of UAEnd UA; ::_thesis: b1 . (x,y) = b2 . (x,y) thus b1 . (x,y) = y * x by A2 .= b2 . (x,y) by A3 ; ::_thesis: verum end; hence b1 = b2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines UAEndComp ENDALG:def_2_:_ for UA being Universal_Algebra for b2 being BinOp of (UAEnd UA) holds ( b2 = UAEndComp UA iff for x, y being Element of UAEnd UA holds b2 . (x,y) = y * x ); definition let UA be Universal_Algebra; func UAEndMonoid UA -> strict multLoopStr means :Def3: :: ENDALG:def 3 ( the carrier of it = UAEnd UA & the multF of it = UAEndComp UA & 1. it = id the carrier of UA ); existence ex b1 being strict multLoopStr st ( the carrier of b1 = UAEnd UA & the multF of b1 = UAEndComp UA & 1. b1 = id the carrier of UA ) proof reconsider i = id the carrier of UA as Element of UAEnd UA by Th2; take multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) ; ::_thesis: ( the carrier of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEnd UA & the multF of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEndComp UA & 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = id the carrier of UA ) thus ( the carrier of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEnd UA & the multF of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = UAEndComp UA & 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = id the carrier of UA ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict multLoopStr st the carrier of b1 = UAEnd UA & the multF of b1 = UAEndComp UA & 1. b1 = id the carrier of UA & the carrier of b2 = UAEnd UA & the multF of b2 = UAEndComp UA & 1. b2 = id the carrier of UA holds b1 = b2 ; end; :: deftheorem Def3 defines UAEndMonoid ENDALG:def_3_:_ for UA being Universal_Algebra for b2 being strict multLoopStr holds ( b2 = UAEndMonoid UA iff ( the carrier of b2 = UAEnd UA & the multF of b2 = UAEndComp UA & 1. b2 = id the carrier of UA ) ); registration let UA be Universal_Algebra; cluster UAEndMonoid UA -> non empty strict ; coherence not UAEndMonoid UA is empty proof reconsider i = id the carrier of UA as Element of UAEnd UA by Th2; set M = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #); 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ; hence not UAEndMonoid UA is empty by Def3; ::_thesis: verum end; end; Lm1: now__::_thesis:_for_UA_being_Universal_Algebra for_x,_e_being_Element_of_(UAEndMonoid_UA)_st_e_=_id_the_carrier_of_UA_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let UA be Universal_Algebra; ::_thesis: for x, e being Element of (UAEndMonoid UA) st e = id the carrier of UA holds ( x * e = x & e * x = x ) let x, e be Element of (UAEndMonoid UA); ::_thesis: ( e = id the carrier of UA implies ( x * e = x & e * x = x ) ) reconsider i = e, y = x as Element of UAEnd UA by Def3; assume A1: e = id the carrier of UA ; ::_thesis: ( x * e = x & e * x = x ) thus x * e = (UAEndComp UA) . (y,i) by Def3 .= i * y by Def2 .= x by A1, FUNCT_2:17 ; ::_thesis: e * x = x thus e * x = (UAEndComp UA) . (i,y) by Def3 .= y * i by Def2 .= x by A1, FUNCT_2:17 ; ::_thesis: verum end; registration let UA be Universal_Algebra; cluster UAEndMonoid UA -> strict associative well-unital ; coherence ( UAEndMonoid UA is well-unital & UAEndMonoid UA is associative ) proof reconsider i = id the carrier of UA as Element of UAEnd UA by Th2; set H = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #); thus UAEndMonoid UA is well-unital ::_thesis: UAEndMonoid UA is associative proof let x be Element of (UAEndMonoid UA); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (UAEndMonoid UA)) = x & (1. (UAEndMonoid UA)) * x = x ) 1. (UAEndMonoid UA) = i by Def3; hence ( x * (1. (UAEndMonoid UA)) = x & (1. (UAEndMonoid UA)) * x = x ) by Lm1; ::_thesis: verum end; for f, g, h being Element of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) holds (f * g) * h = f * (g * h) proof let f, g, h be Element of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #); ::_thesis: (f * g) * h = f * (g * h) reconsider A = f, B = g, C = h as Element of UAEnd UA ; A1: g * h = C * B by Def2; f * g = B * A by Def2; hence (f * g) * h = C * (B * A) by Def2 .= (C * B) * A by RELAT_1:36 .= f * (g * h) by A1, Def2 ; ::_thesis: verum end; then ( 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i & multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) is associative ) by GROUP_1:def_3; hence UAEndMonoid UA is associative by Def3; ::_thesis: verum end; end; theorem Th4: :: ENDALG:4 for UA being Universal_Algebra for x, y being Element of (UAEndMonoid UA) for f, g being Element of UAEnd UA st x = f & y = g holds x * y = g * f proof let UA be Universal_Algebra; ::_thesis: for x, y being Element of (UAEndMonoid UA) for f, g being Element of UAEnd UA st x = f & y = g holds x * y = g * f reconsider i = id the carrier of UA as Element of UAEnd UA by Th2; let x, y be Element of (UAEndMonoid UA); ::_thesis: for f, g being Element of UAEnd UA st x = f & y = g holds x * y = g * f let f, g be Element of UAEnd UA; ::_thesis: ( x = f & y = g implies x * y = g * f ) set H = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #); 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ; then A1: UAEndMonoid UA = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) by Def3; assume ( x = f & y = g ) ; ::_thesis: x * y = g * f hence x * y = g * f by A1, Def2; ::_thesis: verum end; theorem :: ENDALG:5 for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAEndMonoid UA) by Def3; definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; set T = the Sorts of U1; func MSAEnd U1 -> MSFunctionSet of U1,U1 means :Def4: :: ENDALG:def 4 ( ( for f being Element of it holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in it iff h is_homomorphism U1,U1 ) ) ); existence ex b1 being MSFunctionSet of U1,U1 st ( ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in b1 iff h is_homomorphism U1,U1 ) ) ) proof defpred S1[ set ] means ex msf being ManySortedFunction of U1,U1 st ( \$1 = msf & msf is_homomorphism U1,U1 ); consider X being set such that A1: for x being set holds ( x in X iff ( x in MSFuncs ( the Sorts of U1, the Sorts of U1) & S1[x] ) ) from XBOOLE_0:sch_1(); ( id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) & ex F being ManySortedFunction of U1,U1 st ( id the Sorts of U1 = F & F is_homomorphism U1,U1 ) ) by AUTALG_1:20, MSUALG_3:9; then reconsider X = X as non empty set by A1; X c= MSFuncs ( the Sorts of U1, the Sorts of U1) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in MSFuncs ( the Sorts of U1, the Sorts of U1) ) thus ( not q in X or q in MSFuncs ( the Sorts of U1, the Sorts of U1) ) by A1; ::_thesis: verum end; then reconsider X = X as MSFunctionSet of U1,U1 ; take X ; ::_thesis: ( ( for f being Element of X holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in X iff h is_homomorphism U1,U1 ) ) ) thus for f being Element of X holds f is ManySortedFunction of U1,U1 ; ::_thesis: for h being ManySortedFunction of U1,U1 holds ( h in X iff h is_homomorphism U1,U1 ) let h be ManySortedFunction of U1,U1; ::_thesis: ( h in X iff h is_homomorphism U1,U1 ) hereby ::_thesis: ( h is_homomorphism U1,U1 implies h in X ) assume h in X ; ::_thesis: h is_homomorphism U1,U1 then ex msf being ManySortedFunction of U1,U1 st ( h = msf & msf is_homomorphism U1,U1 ) by A1; hence h is_homomorphism U1,U1 ; ::_thesis: verum end; h in MSFuncs ( the Sorts of U1, the Sorts of U1) by AUTALG_1:20; hence ( h is_homomorphism U1,U1 implies h in X ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being MSFunctionSet of U1,U1 st ( for f being Element of b1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in b1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of b2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in b2 iff h is_homomorphism U1,U1 ) ) holds b1 = b2 proof let F1, F2 be MSFunctionSet of U1,U1; ::_thesis: ( ( for f being Element of F1 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in F1 iff h is_homomorphism U1,U1 ) ) & ( for f being Element of F2 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in F2 iff h is_homomorphism U1,U1 ) ) implies F1 = F2 ) assume that A3: for f being Element of F1 holds f is ManySortedFunction of U1,U1 and A4: for h being ManySortedFunction of U1,U1 holds ( h in F1 iff h is_homomorphism U1,U1 ) and A5: for f being Element of F2 holds f is ManySortedFunction of U1,U1 and A6: for h being ManySortedFunction of U1,U1 holds ( h in F2 iff h is_homomorphism U1,U1 ) ; ::_thesis: F1 = F2 A7: F2 c= F1 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F2 or q in F1 ) assume A8: q in F2 ; ::_thesis: q in F1 then reconsider h1 = q as ManySortedFunction of U1,U1 by A5; h1 is_homomorphism U1,U1 by A6, A8; hence q in F1 by A4; ::_thesis: verum end; F1 c= F2 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in F2 ) assume A9: q in F1 ; ::_thesis: q in F2 then reconsider h1 = q as ManySortedFunction of U1,U1 by A3; h1 is_homomorphism U1,U1 by A4, A9; hence q in F2 by A6; ::_thesis: verum end; hence F1 = F2 by A7, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def4 defines MSAEnd ENDALG:def_4_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for b3 being MSFunctionSet of U1,U1 holds ( b3 = MSAEnd U1 iff ( ( for f being Element of b3 holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds ( h in b3 iff h is_homomorphism U1,U1 ) ) ) ); theorem :: ENDALG:6 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds MSAEnd U1 c= MSFuncs ( the Sorts of U1, the Sorts of U1) ; theorem Th7: :: ENDALG:7 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAEnd U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 in MSAEnd U1 let U1 be non-empty MSAlgebra over S; ::_thesis: id the Sorts of U1 in MSAEnd U1 id the Sorts of U1 is_homomorphism U1,U1 by MSUALG_3:9; hence id the Sorts of U1 in MSAEnd U1 by Def4; ::_thesis: verum end; theorem Th8: :: ENDALG:8 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1 let U1 be non-empty MSAlgebra over S; ::_thesis: for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1 let f1, f2 be Element of MSAEnd U1; ::_thesis: f1 ** f2 in MSAEnd U1 ( f1 is_homomorphism U1,U1 & f2 is_homomorphism U1,U1 ) by Def4; then f1 ** f2 is_homomorphism U1,U1 by MSUALG_3:10; hence f1 ** f2 in MSAEnd U1 by Def4; ::_thesis: verum end; theorem Th9: :: ENDALG:9 for UA being Universal_Algebra for F being ManySortedFunction of (MSAlg UA),(MSAlg UA) for f being Element of UAEnd UA st F = 0 .--> f holds F in MSAEnd (MSAlg UA) proof let UA be Universal_Algebra; ::_thesis: for F being ManySortedFunction of (MSAlg UA),(MSAlg UA) for f being Element of UAEnd UA st F = 0 .--> f holds F in MSAEnd (MSAlg UA) let F be ManySortedFunction of (MSAlg UA),(MSAlg UA); ::_thesis: for f being Element of UAEnd UA st F = 0 .--> f holds F in MSAEnd (MSAlg UA) let f be Element of UAEnd UA; ::_thesis: ( F = 0 .--> f implies F in MSAEnd (MSAlg UA) ) assume F = 0 .--> f ; ::_thesis: F in MSAEnd (MSAlg UA) then A1: F = MSAlg f by MSUHOM_1:def_3; f is_homomorphism UA,UA by Def1; then MSAlg f is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:16; then F is_homomorphism MSAlg UA, MSAlg UA by A1, MSUHOM_1:9; hence F in MSAEnd (MSAlg UA) by Def4; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; func MSAEndComp U1 -> BinOp of (MSAEnd U1) means :Def5: :: ENDALG:def 5 for x, y being Element of MSAEnd U1 holds it . (x,y) = y ** x; existence ex b1 being BinOp of (MSAEnd U1) st for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x proof defpred S1[ Element of MSAEnd U1, Element of MSAEnd U1, set ] means \$3 = \$2 ** \$1; A1: for x, y being Element of MSAEnd U1 ex m being Element of MSAEnd U1 st S1[x,y,m] proof let x, y be Element of MSAEnd U1; ::_thesis: ex m being Element of MSAEnd U1 st S1[x,y,m] reconsider xx = x, yy = y as ManySortedFunction of U1,U1 ; reconsider m = yy ** xx as Element of MSAEnd U1 by Th8; take m ; ::_thesis: S1[x,y,m] thus S1[x,y,m] ; ::_thesis: verum end; ex B being BinOp of (MSAEnd U1) st for x, y being Element of MSAEnd U1 holds S1[x,y,B . (x,y)] from BINOP_1:sch_3(A1); hence ex b1 being BinOp of (MSAEnd U1) st for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (MSAEnd U1) st ( for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b2 . (x,y) = y ** x ) holds b1 = b2 proof let b1, b2 be BinOp of (MSAEnd U1); ::_thesis: ( ( for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x ) & ( for x, y being Element of MSAEnd U1 holds b2 . (x,y) = y ** x ) implies b1 = b2 ) assume that A2: for x, y being Element of MSAEnd U1 holds b1 . (x,y) = y ** x and A3: for x, y being Element of MSAEnd U1 holds b2 . (x,y) = y ** x ; ::_thesis: b1 = b2 for x, y being Element of MSAEnd U1 holds b1 . (x,y) = b2 . (x,y) proof let x, y be Element of MSAEnd U1; ::_thesis: b1 . (x,y) = b2 . (x,y) thus b1 . (x,y) = y ** x by A2 .= b2 . (x,y) by A3 ; ::_thesis: verum end; hence b1 = b2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines MSAEndComp ENDALG:def_5_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for b3 being BinOp of (MSAEnd U1) holds ( b3 = MSAEndComp U1 iff for x, y being Element of MSAEnd U1 holds b3 . (x,y) = y ** x ); definition let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; func MSAEndMonoid U1 -> strict multLoopStr means :Def6: :: ENDALG:def 6 ( the carrier of it = MSAEnd U1 & the multF of it = MSAEndComp U1 & 1. it = id the Sorts of U1 ); existence ex b1 being strict multLoopStr st ( the carrier of b1 = MSAEnd U1 & the multF of b1 = MSAEndComp U1 & 1. b1 = id the Sorts of U1 ) proof reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7; take H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); ::_thesis: ( the carrier of H = MSAEnd U1 & the multF of H = MSAEndComp U1 & 1. H = id the Sorts of U1 ) thus the carrier of H = MSAEnd U1 ; ::_thesis: ( the multF of H = MSAEndComp U1 & 1. H = id the Sorts of U1 ) thus the multF of H = MSAEndComp U1 ; ::_thesis: 1. H = id the Sorts of U1 thus 1. H = id the Sorts of U1 ; ::_thesis: verum end; uniqueness for b1, b2 being strict multLoopStr st the carrier of b1 = MSAEnd U1 & the multF of b1 = MSAEndComp U1 & 1. b1 = id the Sorts of U1 & the carrier of b2 = MSAEnd U1 & the multF of b2 = MSAEndComp U1 & 1. b2 = id the Sorts of U1 holds b1 = b2 ; end; :: deftheorem Def6 defines MSAEndMonoid ENDALG:def_6_:_ for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for b3 being strict multLoopStr holds ( b3 = MSAEndMonoid U1 iff ( the carrier of b3 = MSAEnd U1 & the multF of b3 = MSAEndComp U1 & 1. b3 = id the Sorts of U1 ) ); registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; cluster MSAEndMonoid U1 -> non empty strict ; coherence not MSAEndMonoid U1 is empty proof reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7; set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i ; hence not MSAEndMonoid U1 is empty by Def6; ::_thesis: verum end; end; Lm2: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_U1_being_non-empty_MSAlgebra_over_S for_x,_e_being_Element_of_(MSAEndMonoid_U1)_st_e_=_id_the_Sorts_of_U1_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for x, e being Element of (MSAEndMonoid U1) st e = id the Sorts of U1 holds ( x * e = x & e * x = x ) let U1 be non-empty MSAlgebra over S; ::_thesis: for x, e being Element of (MSAEndMonoid U1) st e = id the Sorts of U1 holds ( x * e = x & e * x = x ) set F = MSAEndMonoid U1; let x, e be Element of (MSAEndMonoid U1); ::_thesis: ( e = id the Sorts of U1 implies ( x * e = x & e * x = x ) ) reconsider i = e, y = x as Element of MSAEnd U1 by Def6; assume A1: e = id the Sorts of U1 ; ::_thesis: ( x * e = x & e * x = x ) thus x * e = (MSAEndComp U1) . (y,i) by Def6 .= i ** y by Def5 .= x by A1, MSUALG_3:4 ; ::_thesis: e * x = x thus e * x = (MSAEndComp U1) . (i,y) by Def6 .= y ** i by Def5 .= x by A1, MSUALG_3:3 ; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; cluster MSAEndMonoid U1 -> strict associative well-unital ; coherence ( MSAEndMonoid U1 is well-unital & MSAEndMonoid U1 is associative ) proof reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7; set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); thus MSAEndMonoid U1 is well-unital ::_thesis: MSAEndMonoid U1 is associative proof let x be Element of (MSAEndMonoid U1); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (MSAEndMonoid U1)) = x & (1. (MSAEndMonoid U1)) * x = x ) 1. (MSAEndMonoid U1) = i by Def6; hence ( x * (1. (MSAEndMonoid U1)) = x & (1. (MSAEndMonoid U1)) * x = x ) by Lm2; ::_thesis: verum end; for f, g, h being Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) holds (f * g) * h = f * (g * h) proof let f, g, h be Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); ::_thesis: (f * g) * h = f * (g * h) reconsider A = f, B = g, C = h as Element of MSAEnd U1 ; A1: g * h = C ** B by Def5; f * g = B ** A by Def5; hence (f * g) * h = C ** (B ** A) by Def5 .= (C ** B) ** A by PBOOLE:140 .= f * (g * h) by A1, Def5 ; ::_thesis: verum end; then ( 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i & multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) is associative ) by GROUP_1:def_3; hence MSAEndMonoid U1 is associative by Def6; ::_thesis: verum end; end; theorem Th10: :: ENDALG:10 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for x, y being Element of (MSAEndMonoid U1) for f, g being Element of MSAEnd U1 st x = f & y = g holds x * y = g ** f proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for x, y being Element of (MSAEndMonoid U1) for f, g being Element of MSAEnd U1 st x = f & y = g holds x * y = g ** f let U1 be non-empty MSAlgebra over S; ::_thesis: for x, y being Element of (MSAEndMonoid U1) for f, g being Element of MSAEnd U1 st x = f & y = g holds x * y = g ** f reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7; let x, y be Element of (MSAEndMonoid U1); ::_thesis: for f, g being Element of MSAEnd U1 st x = f & y = g holds x * y = g ** f let f, g be Element of MSAEnd U1; ::_thesis: ( x = f & y = g implies x * y = g ** f ) set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i ; then A1: MSAEndMonoid U1 = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) by Def6; assume ( x = f & y = g ) ; ::_thesis: x * y = g ** f hence x * y = g ** f by A1, Def5; ::_thesis: verum end; theorem :: ENDALG:11 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S holds id the Sorts of U1 = 1_ (MSAEndMonoid U1) by Def6; theorem Th12: :: ENDALG:12 for UA being Universal_Algebra for f being Element of UAEnd UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) proof let UA be Universal_Algebra; ::_thesis: for f being Element of UAEnd UA holds 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) let f be Element of UAEnd UA; ::_thesis: 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) MSAlg f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:9; hence 0 .--> f is ManySortedFunction of (MSAlg UA),(MSAlg UA) by MSUHOM_1:def_3; ::_thesis: verum end; Lm3: for UA being Universal_Algebra for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) holds rng h = MSAEnd (MSAlg UA) proof let UA be Universal_Algebra; ::_thesis: for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) holds rng h = MSAEnd (MSAlg UA) let h be Function; ::_thesis: ( dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) implies rng h = MSAEnd (MSAlg UA) ) assume that A1: dom h = UAEnd UA and A2: for x being set st x in UAEnd UA holds h . x = 0 .--> x ; ::_thesis: rng h = MSAEnd (MSAlg UA) A3: MSAEnd (MSAlg UA) c= rng h proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MSAEnd (MSAlg UA) or x in rng h ) assume A4: x in MSAEnd (MSAlg UA) ; ::_thesis: x in rng h then reconsider f = x as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Def4; the carrier of (MSSign UA) = {0} by MSUALG_1:def_8; then A5: f = 0 .--> (f . 0) by AUTALG_1:11; A6: f is_homomorphism MSAlg UA, MSAlg UA by A4, Def4; ex q being set st ( q in dom h & x = h . q ) proof take q = f . 0; ::_thesis: ( q in dom h & x = h . q ) f is ManySortedFunction of (MSAlg UA),((MSAlg UA) Over (MSSign UA)) by MSUHOM_1:9; then reconsider q9 = q as Function of UA,UA by AUTALG_1:31; MSAlg q9 = f by A5, MSUHOM_1:def_3; then MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by A6, MSUHOM_1:9; then q9 is_homomorphism UA,UA by MSUHOM_1:21; hence q in dom h by A1, Def1; ::_thesis: x = h . q hence x = h . q by A1, A2, A5; ::_thesis: verum end; hence x in rng h by FUNCT_1:def_3; ::_thesis: verum end; rng h c= MSAEnd (MSAlg UA) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng h or x in MSAEnd (MSAlg UA) ) assume x in rng h ; ::_thesis: x in MSAEnd (MSAlg UA) then consider q being set such that A7: q in dom h and A8: x = h . q by FUNCT_1:def_3; consider q9 being Element of UAEnd UA such that A9: q9 = q by A1, A7; ( x = 0 .--> q & 0 .--> q is ManySortedFunction of (MSAlg UA),(MSAlg UA) ) by A1, A2, A7, A8, Th12; then consider d being ManySortedFunction of (MSAlg UA),(MSAlg UA) such that A10: d = x ; q9 is_homomorphism UA,UA by Def1; then A11: MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:16; MSAlg q9 = 0 .--> q by A9, MSUHOM_1:def_3 .= x by A1, A2, A7, A8 ; then d is_homomorphism MSAlg UA, MSAlg UA by A10, A11, MSUHOM_1:9; hence x in MSAEnd (MSAlg UA) by A10, Def4; ::_thesis: verum end; hence rng h = MSAEnd (MSAlg UA) by A3, XBOOLE_0:def_10; ::_thesis: verum end; registration cluster non empty left_unital for multLoopStr ; existence ex b1 being non empty multLoopStr st b1 is left_unital proof set m = the BinOp of {0}; set u = the Element of {0}; take multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #) ; ::_thesis: multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #) is left_unital let x be Element of multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #); :: according to VECTSP_1:def_8 ::_thesis: (1. multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #)) * x = x thus (1. multLoopStr(# {0}, the BinOp of {0}, the Element of {0} #)) * x = 0 by TARSKI:def_1 .= x by TARSKI:def_1 ; ::_thesis: verum end; end; registration let G, H be non empty well-unital multLoopStr ; cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving multiplicative for Element of bool [: the carrier of G, the carrier of H:]; existence ex b1 being Function of G,H st ( b1 is multiplicative & b1 is unity-preserving ) proof reconsider m = the carrier of G --> (1. H) as Function of the carrier of G, the carrier of H ; reconsider m = m as Function of G,H ; take m ; ::_thesis: ( m is multiplicative & m is unity-preserving ) for x, y being Element of G holds m . (x * y) = (m . x) * (m . y) proof let x, y be Element of G; ::_thesis: m . (x * y) = (m . x) * (m . y) m . (x * y) = 1. H by FUNCOP_1:7 .= (1. H) * (1. H) by VECTSP_1:def_8 .= (m . x) * (1. H) by FUNCOP_1:7 .= (m . x) * (m . y) by FUNCOP_1:7 ; hence m . (x * y) = (m . x) * (m . y) ; ::_thesis: verum end; hence m is multiplicative by GROUP_6:def_6; ::_thesis: m is unity-preserving thus m . (1_ G) = 1_ H by FUNCOP_1:7; :: according to GROUP_1:def_13 ::_thesis: verum end; end; definition let G, H be non empty well-unital multLoopStr ; mode Homomorphism of G,H is unity-preserving multiplicative Function of G,H; end; theorem Th13: :: ENDALG:13 for G being non empty well-unital multLoopStr holds id the carrier of G is Homomorphism of G,G proof let G be non empty well-unital multLoopStr ; ::_thesis: id the carrier of G is Homomorphism of G,G reconsider f = id the carrier of G as Function of G,G ; A1: for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) proof let a, b be Element of G; ::_thesis: f . (a * b) = (f . a) * (f . b) f . (a * b) = a * b by FUNCT_1:18 .= (f . a) * b by FUNCT_1:18 .= (f . a) * (f . b) by FUNCT_1:18 ; hence f . (a * b) = (f . a) * (f . b) ; ::_thesis: verum end; f . (1_ G) = 1_ G by FUNCT_1:18; hence id the carrier of G is Homomorphism of G,G by A1, GROUP_1:def_13, GROUP_6:def_6; ::_thesis: verum end; definition let G, H be non empty well-unital multLoopStr ; predG,H are_isomorphic means :Def7: :: ENDALG:def 7 ex h being Homomorphism of G,H st h is bijective ; reflexivity for G being non empty well-unital multLoopStr ex h being Homomorphism of G,G st h is bijective proof let G be non empty well-unital multLoopStr ; ::_thesis: ex h being Homomorphism of G,G st h is bijective reconsider i = id the carrier of G as Homomorphism of G,G by Th13; A1: the carrier of G c= rng i proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng i ) assume A2: y in the carrier of G ; ::_thesis: y in rng i ex x being set st ( x in dom i & y = i . x ) proof take y ; ::_thesis: ( y in dom i & y = i . y ) thus ( y in dom i & y = i . y ) by A2, FUNCT_1:17; ::_thesis: verum end; hence y in rng i by FUNCT_1:def_3; ::_thesis: verum end; rng i c= the carrier of G by RELAT_1:def_19; then rng i = the carrier of G by A1, XBOOLE_0:def_10; then i is onto by FUNCT_2:def_3; hence ex h being Homomorphism of G,G st h is bijective ; ::_thesis: verum end; end; :: deftheorem Def7 defines are_isomorphic ENDALG:def_7_:_ for G, H being non empty well-unital multLoopStr holds ( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective ); theorem Th14: :: ENDALG:14 for UA being Universal_Algebra for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) holds h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) proof let UA be Universal_Algebra; ::_thesis: for h being Function st dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) holds h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) reconsider i = id the Sorts of (MSAlg UA) as Element of MSAEnd (MSAlg UA) by Th7; set G = UAEndMonoid UA; set H = MSAEndMonoid (MSAlg UA); set M = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #); reconsider e = id the carrier of UA as Element of UAEnd UA by Th2; let h be Function; ::_thesis: ( dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) implies h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) ) assume that A1: dom h = UAEnd UA and A2: for x being set st x in UAEnd UA holds h . x = 0 .--> x ; ::_thesis: h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) A3: the carrier of (UAEndMonoid UA) = dom h by A1, Def3; 1. multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #) = i ; then A4: MSAEndMonoid (MSAlg UA) = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),i #) by Def6; then rng h c= the carrier of (MSAEndMonoid (MSAlg UA)) by A1, A2, Lm3; then reconsider h9 = h as Function of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A3, FUNCT_2:def_1, RELSET_1:4; A5: h9 . e = 0 .--> e by A2; A6: for a, b being Element of (UAEndMonoid UA) holds h9 . (a * b) = (h9 . a) * (h9 . b) proof let a, b be Element of (UAEndMonoid UA); ::_thesis: h9 . (a * b) = (h9 . a) * (h9 . b) reconsider a9 = a, b9 = b as Element of UAEnd UA by Def3; reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Th12; reconsider ha = h9 . a, hb = h9 . b as Element of MSAEnd (MSAlg UA) by Def6; A7: h9 . (b9 * a9) = 0 .--> (b9 * a9) by A2, Th3; reconsider A9 = A, B9 = B as Element of (MSAEndMonoid (MSAlg UA)) by A4, Th9; A8: ( ha = A9 & hb = B9 ) by A2; thus h9 . (a * b) = h9 . (b9 * a9) by Th4 .= MSAlg (b9 * a9) by A7, MSUHOM_1:def_3 .= (MSAlg b9) ** (MSAlg a9) by MSUHOM_1:26 .= B ** (MSAlg a9) by MSUHOM_1:def_3 .= B ** A by MSUHOM_1:def_3 .= (h9 . a) * (h9 . b) by A8, Th10 ; ::_thesis: verum end; h9 . (1. (UAEndMonoid UA)) = h9 . e by Def3 .= MSAlg e by A5, MSUHOM_1:def_3 .= i by MSUHOM_1:25 .= 1_ (MSAEndMonoid (MSAlg UA)) by Def6 ; then h9 . (1_ (UAEndMonoid UA)) = 1_ (MSAEndMonoid (MSAlg UA)) ; hence h is Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A6, GROUP_1:def_13, GROUP_6:def_6; ::_thesis: verum end; theorem Th15: :: ENDALG:15 for UA being Universal_Algebra for h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) holds h is bijective proof let UA be Universal_Algebra; ::_thesis: for h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) holds h is bijective reconsider e = id the Sorts of (MSAlg UA) as Element of MSAEnd (MSAlg UA) by Th7; set N = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #); reconsider i = id the carrier of UA as Element of UAEnd UA by Th2; let h be Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)); ::_thesis: ( ( for x being set st x in UAEnd UA holds h . x = 0 .--> x ) implies h is bijective ) set G = UAEndMonoid UA; set H = MSAEndMonoid (MSAlg UA); set M = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #); 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ; then A1: UAEndMonoid UA = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) by Def3; assume A2: for x being set st x in UAEnd UA holds h . x = 0 .--> x ; ::_thesis: h is bijective for a, b being Element of (UAEndMonoid UA) st h . a = h . b holds a = b proof let a, b be Element of (UAEndMonoid UA); ::_thesis: ( h . a = h . b implies a = b ) assume A3: h . a = h . b ; ::_thesis: a = b A4: h . b = 0 .--> b by A2, A1 .= [:{0},{b}:] ; h . a = 0 .--> a by A2, A1 .= [:{0},{a}:] ; then {a} = {b} by A3, A4, ZFMISC_1:110; hence a = b by ZFMISC_1:3; ::_thesis: verum end; then A5: h is one-to-one by GROUP_6:1; 1. multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #) = e ; then A6: MSAEndMonoid (MSAlg UA) = multLoopStr(# (MSAEnd (MSAlg UA)),(MSAEndComp (MSAlg UA)),e #) by Def6; dom h = UAEnd UA by A1, FUNCT_2:def_1; then rng h = the carrier of (MSAEndMonoid (MSAlg UA)) by A2, A6, Lm3; then h is onto by FUNCT_2:def_3; hence h is bijective by A5; ::_thesis: verum end; theorem :: ENDALG:16 for UA being Universal_Algebra holds UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic proof let UA be Universal_Algebra; ::_thesis: UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic set G = UAEndMonoid UA; set H = MSAEndMonoid (MSAlg UA); ex h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st h is bijective proof deffunc H1( set ) -> set = 0 .--> \$1; consider h being Function such that A1: ( dom h = UAEnd UA & ( for x being set st x in UAEnd UA holds h . x = H1(x) ) ) from FUNCT_1:sch_3(); reconsider h = h as Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) by A1, Th14; h is bijective by A1, Th15; hence ex h being Homomorphism of (UAEndMonoid UA),(MSAEndMonoid (MSAlg UA)) st h is bijective ; ::_thesis: verum end; hence UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic by Def7; ::_thesis: verum end;