:: MSUHOM_1 semantic presentation begin theorem Th1: :: MSUHOM_1:1 for f, g being Function for C being set st rng f c= C holds (g | C) * f = g * f proof let f, g be Function; ::_thesis: for C being set st rng f c= C holds (g | C) * f = g * f let C be set ; ::_thesis: ( rng f c= C implies (g | C) * f = g * f ) assume A1: rng f c= C ; ::_thesis: (g | C) * f = g * f (g | C) * f = g * (C |` f) by MONOID_1:1 .= g * f by A1, RELAT_1:94 ; hence (g | C) * f = g * f ; ::_thesis: verum end; theorem Th2: :: MSUHOM_1:2 for I being set for C being Subset of I holds C * c= I * proof let I be set ; ::_thesis: for C being Subset of I holds C * c= I * let C be Subset of I; ::_thesis: C * c= I * thus C * c= I * ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in C * or a in I * ) assume a in C * ; ::_thesis: a in I * then reconsider p = a as FinSequence of C by FINSEQ_1:def_11; rng p c= I by XBOOLE_1:1; then p is FinSequence of I by FINSEQ_1:def_4; hence a in I * by FINSEQ_1:def_11; ::_thesis: verum end; end; theorem :: MSUHOM_1:3 for f being Function for C being set st f is Function-yielding holds f | C is Function-yielding ; theorem Th4: :: MSUHOM_1:4 for I being set for C being Subset of I for M being ManySortedSet of I holds (M | C) # = (M #) | (C *) proof let I be set ; ::_thesis: for C being Subset of I for M being ManySortedSet of I holds (M | C) # = (M #) | (C *) let C be Subset of I; ::_thesis: for M being ManySortedSet of I holds (M | C) # = (M #) | (C *) let M be ManySortedSet of I; ::_thesis: (M | C) # = (M #) | (C *) dom (M #) = I * by PARTFUN1:def_2; then dom ((M #) | (C *)) = C * by Th2, RELAT_1:62; then reconsider D = (M #) | (C *) as ManySortedSet of C * by PARTFUN1:def_2; A1: C * c= I * by Th2; for i being Element of C * holds ((M #) | (C *)) . i = product ((M | C) * i) proof let i be Element of C * ; ::_thesis: ((M #) | (C *)) . i = product ((M | C) * i) A2: rng i c= C ; i in C * ; then A3: i in dom D by PARTFUN1:def_2; A4: i in I * by A1, TARSKI:def_3; for a being set holds ( a in D . i iff ex g being Function st ( a = g & dom g = dom ((M | C) * i) & ( for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ) ) ) proof let a be set ; ::_thesis: ( a in D . i iff ex g being Function st ( a = g & dom g = dom ((M | C) * i) & ( for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ) ) ) hereby ::_thesis: ( ex g being Function st ( a = g & dom g = dom ((M | C) * i) & ( for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ) ) implies a in D . i ) assume a in D . i ; ::_thesis: ex g being Function st ( a = g & dom g = dom ((M | C) * i) & ( for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ) ) then a in (M #) . i by A3, FUNCT_1:47; then a in product (M * i) by A4, FINSEQ_2:def_5; then consider g being Function such that A5: a = g and A6: dom g = dom (M * i) and A7: for x being set st x in dom (M * i) holds g . x in (M * i) . x by CARD_3:def_5; take g = g; ::_thesis: ( a = g & dom g = dom ((M | C) * i) & ( for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ) ) thus a = g by A5; ::_thesis: ( dom g = dom ((M | C) * i) & ( for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ) ) rng i c= C ; hence dom g = dom ((M | C) * i) by A6, Th1; ::_thesis: for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a thus for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ::_thesis: verum proof A8: rng i c= C ; let a be set ; ::_thesis: ( a in dom ((M | C) * i) implies g . a in ((M | C) * i) . a ) assume a in dom ((M | C) * i) ; ::_thesis: g . a in ((M | C) * i) . a then a in dom (M * i) by A8, Th1; then g . a in (M * i) . a by A7; hence g . a in ((M | C) * i) . a by A8, Th1; ::_thesis: verum end; end; given g being Function such that A9: a = g and A10: dom g = dom ((M | C) * i) and A11: for a being set st a in dom ((M | C) * i) holds g . a in ((M | C) * i) . a ; ::_thesis: a in D . i A12: for a being set st a in dom (M * i) holds g . a in (M * i) . a proof let a be set ; ::_thesis: ( a in dom (M * i) implies g . a in (M * i) . a ) assume a in dom (M * i) ; ::_thesis: g . a in (M * i) . a then a in dom ((M | C) * i) by A2, Th1; then g . a in ((M | C) * i) . a by A11; hence g . a in (M * i) . a by A2, Th1; ::_thesis: verum end; dom g = dom (M * i) by A2, A10, Th1; then a in product (M * i) by A9, A12, CARD_3:def_5; then a in (M #) . i by A4, FINSEQ_2:def_5; hence a in D . i by A3, FUNCT_1:47; ::_thesis: verum end; hence ((M #) | (C *)) . i = product ((M | C) * i) by CARD_3:def_5; ::_thesis: verum end; hence (M | C) # = D by FINSEQ_2:def_5 .= (M #) | (C *) ; ::_thesis: verum end; definition let S, S9 be non empty ManySortedSign ; predS <= S9 means :Def1: :: MSUHOM_1:def 1 ( the carrier of S c= the carrier of S9 & the carrier' of S c= the carrier' of S9 & the Arity of S9 | the carrier' of S = the Arity of S & the ResultSort of S9 | the carrier' of S = the ResultSort of S ); reflexivity for S being non empty ManySortedSign holds ( the carrier of S c= the carrier of S & the carrier' of S c= the carrier' of S & the Arity of S | the carrier' of S = the Arity of S & the ResultSort of S | the carrier' of S = the ResultSort of S ) proof let S be non empty ManySortedSign ; ::_thesis: ( the carrier of S c= the carrier of S & the carrier' of S c= the carrier' of S & the Arity of S | the carrier' of S = the Arity of S & the ResultSort of S | the carrier' of S = the ResultSort of S ) thus ( the carrier of S c= the carrier of S & the carrier' of S c= the carrier' of S & the Arity of S | the carrier' of S = the Arity of S & the ResultSort of S | the carrier' of S = the ResultSort of S ) ; ::_thesis: verum end; end; :: deftheorem Def1 defines <= MSUHOM_1:def_1_:_ for S, S9 being non empty ManySortedSign holds ( S <= S9 iff ( the carrier of S c= the carrier of S9 & the carrier' of S c= the carrier' of S9 & the Arity of S9 | the carrier' of S = the Arity of S & the ResultSort of S9 | the carrier' of S = the ResultSort of S ) ); theorem :: MSUHOM_1:5 for S, S9, S99 being non empty ManySortedSign st S <= S9 & S9 <= S99 holds S <= S99 proof let S, S9, S99 be non empty ManySortedSign ; ::_thesis: ( S <= S9 & S9 <= S99 implies S <= S99 ) assume that A1: S <= S9 and A2: S9 <= S99 ; ::_thesis: S <= S99 ( the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier of S99 ) by A1, A2, Def1; hence the carrier of S c= the carrier of S99 by XBOOLE_1:1; :: according to MSUHOM_1:def_1 ::_thesis: ( the carrier' of S c= the carrier' of S99 & the Arity of S99 | the carrier' of S = the Arity of S & the ResultSort of S99 | the carrier' of S = the ResultSort of S ) A3: the carrier' of S c= the carrier' of S9 by A1, Def1; the carrier' of S9 c= the carrier' of S99 by A2, Def1; hence the carrier' of S c= the carrier' of S99 by A3, XBOOLE_1:1; ::_thesis: ( the Arity of S99 | the carrier' of S = the Arity of S & the ResultSort of S99 | the carrier' of S = the ResultSort of S ) thus the Arity of S99 | the carrier' of S = the Arity of S99 | ( the carrier' of S9 /\ the carrier' of S) by A3, XBOOLE_1:28 .= ( the Arity of S99 | the carrier' of S9) | the carrier' of S by RELAT_1:71 .= the Arity of S9 | the carrier' of S by A2, Def1 .= the Arity of S by A1, Def1 ; ::_thesis: the ResultSort of S99 | the carrier' of S = the ResultSort of S thus the ResultSort of S99 | the carrier' of S = the ResultSort of S99 | ( the carrier' of S9 /\ the carrier' of S) by A3, XBOOLE_1:28 .= ( the ResultSort of S99 | the carrier' of S9) | the carrier' of S by RELAT_1:71 .= the ResultSort of S9 | the carrier' of S by A2, Def1 .= the ResultSort of S by A1, Def1 ; ::_thesis: verum end; theorem :: MSUHOM_1:6 for S, S9 being non empty strict ManySortedSign st S <= S9 & S9 <= S holds S = S9 proof let S, S9 be non empty strict ManySortedSign ; ::_thesis: ( S <= S9 & S9 <= S implies S = S9 ) assume that A1: S <= S9 and A2: S9 <= S ; ::_thesis: S = S9 A3: the carrier' of S9 c= the carrier' of S by A2, Def1; A4: dom the ResultSort of S9 = the carrier' of S9 by FUNCT_2:def_1; the ResultSort of S9 | the carrier' of S = the ResultSort of S by A1, Def1; then A5: the ResultSort of S = the ResultSort of S9 by A3, A4, RELAT_1:68; A6: dom the Arity of S9 = the carrier' of S9 by FUNCT_2:def_1; the Arity of S9 | the carrier' of S = the Arity of S by A1, Def1; then A7: the Arity of S = the Arity of S9 by A3, A6, RELAT_1:68; the carrier' of S c= the carrier' of S9 by A1, Def1; then A8: the carrier' of S = the carrier' of S9 by A3, XBOOLE_0:def_10; ( the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier of S ) by A1, A2, Def1; hence S = S9 by A8, A7, A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MSUHOM_1:7 for n being Nat for A being non empty set for g being Function for a being Element of A for k being Nat st 1 <= k & k <= n holds (a .--> g) . ((n |-> a) /. k) = g proof let n be Nat; ::_thesis: for A being non empty set for g being Function for a being Element of A for k being Nat st 1 <= k & k <= n holds (a .--> g) . ((n |-> a) /. k) = g let A be non empty set ; ::_thesis: for g being Function for a being Element of A for k being Nat st 1 <= k & k <= n holds (a .--> g) . ((n |-> a) /. k) = g let g be Function; ::_thesis: for a being Element of A for k being Nat st 1 <= k & k <= n holds (a .--> g) . ((n |-> a) /. k) = g let a be Element of A; ::_thesis: for k being Nat st 1 <= k & k <= n holds (a .--> g) . ((n |-> a) /. k) = g let k be Nat; ::_thesis: ( 1 <= k & k <= n implies (a .--> g) . ((n |-> a) /. k) = g ) assume ( 1 <= k & k <= n ) ; ::_thesis: (a .--> g) . ((n |-> a) /. k) = g then A1: k in Seg n by FINSEQ_1:1; then k in dom (n |-> a) by FUNCOP_1:13; then (n |-> a) /. k = (n |-> a) . k by PARTFUN1:def_6 .= a by A1, FUNCOP_1:7 ; hence (a .--> g) . ((n |-> a) /. k) = g by FUNCOP_1:72; ::_thesis: verum end; theorem Th8: :: MSUHOM_1:8 for I being set for I0 being Subset of I for A, B being ManySortedSet of I for F being ManySortedFunction of A,B for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds F | I0 is ManySortedFunction of A0,B0 proof let I be set ; ::_thesis: for I0 being Subset of I for A, B being ManySortedSet of I for F being ManySortedFunction of A,B for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds F | I0 is ManySortedFunction of A0,B0 let I0 be Subset of I; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of A,B for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds F | I0 is ManySortedFunction of A0,B0 let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds F | I0 is ManySortedFunction of A0,B0 let F be ManySortedFunction of A,B; ::_thesis: for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds F | I0 is ManySortedFunction of A0,B0 let A0, B0 be ManySortedSet of I0; ::_thesis: ( A0 = A | I0 & B0 = B | I0 implies F | I0 is ManySortedFunction of A0,B0 ) assume that A1: A0 = A | I0 and A2: B0 = B | I0 ; ::_thesis: F | I0 is ManySortedFunction of A0,B0 reconsider G = F | I0 as ManySortedFunction of I0 ; A3: ( dom A0 = I0 & dom (F | I0) = I0 ) by PARTFUN1:def_2; A4: dom B0 = I0 by PARTFUN1:def_2; now__::_thesis:_for_i_being_set_st_i_in_I0_holds_ G_._i_is_Function_of_(A0_._i),(B0_._i) let i be set ; ::_thesis: ( i in I0 implies G . i is Function of (A0 . i),(B0 . i) ) assume A5: i in I0 ; ::_thesis: G . i is Function of (A0 . i),(B0 . i) then A6: B . i = B0 . i by A2, A4, FUNCT_1:47; ( G . i = F . i & A . i = A0 . i ) by A1, A3, A5, FUNCT_1:47; hence G . i is Function of (A0 . i),(B0 . i) by A5, A6, PBOOLE:def_15; ::_thesis: verum end; hence F | I0 is ManySortedFunction of A0,B0 by PBOOLE:def_15; ::_thesis: verum end; definition let S, S9 be non empty non void strict ManySortedSign ; let A be strict non-empty MSAlgebra over S9; assume A1: S <= S9 ; funcA Over S -> strict non-empty MSAlgebra over S means :Def2: :: MSUHOM_1:def 2 ( the Sorts of it = the Sorts of A | the carrier of S & the Charact of it = the Charact of A | the carrier' of S ); existence ex b1 being strict non-empty MSAlgebra over S st ( the Sorts of b1 = the Sorts of A | the carrier of S & the Charact of b1 = the Charact of A | the carrier' of S ) proof set D = the Charact of A | the carrier' of S; set C = the Sorts of A | the carrier of S; A2: rng the Arity of S c= the carrier of S * ; A3: the carrier' of S c= the carrier' of S9 by A1, Def1; then reconsider D = the Charact of A | the carrier' of S as ManySortedSet of the carrier' of S ; A4: the carrier of S c= the carrier of S9 by A1, Def1; then reconsider C = the Sorts of A | the carrier of S as ManySortedSet of the carrier of S ; rng the ResultSort of S c= the carrier of S ; then A5: C * the ResultSort of S = the Sorts of A * the ResultSort of S by Th1 .= the Sorts of A * ( the ResultSort of S9 | the carrier' of S) by A1, Def1 .= ( the Sorts of A * the ResultSort of S9) | the carrier' of S by RELAT_1:83 ; (C #) * the Arity of S = (( the Sorts of A #) | ( the carrier of S *)) * the Arity of S by A4, Th4 .= ( the Sorts of A #) * the Arity of S by A2, Th1 .= ( the Sorts of A #) * ( the Arity of S9 | the carrier' of S) by A1, Def1 .= (( the Sorts of A #) * the Arity of S9) | the carrier' of S by RELAT_1:83 ; then reconsider D = D as ManySortedFunction of (C #) * the Arity of S,C * the ResultSort of S by A3, A5, Th8; reconsider B = MSAlgebra(# C,D #) as strict non-empty MSAlgebra over S by MSUALG_1:def_3; take B ; ::_thesis: ( the Sorts of B = the Sorts of A | the carrier of S & the Charact of B = the Charact of A | the carrier' of S ) thus ( the Sorts of B = the Sorts of A | the carrier of S & the Charact of B = the Charact of A | the carrier' of S ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict non-empty MSAlgebra over S st the Sorts of b1 = the Sorts of A | the carrier of S & the Charact of b1 = the Charact of A | the carrier' of S & the Sorts of b2 = the Sorts of A | the carrier of S & the Charact of b2 = the Charact of A | the carrier' of S holds b1 = b2 ; end; :: deftheorem Def2 defines Over MSUHOM_1:def_2_:_ for S, S9 being non empty non void strict ManySortedSign for A being strict non-empty MSAlgebra over S9 st S <= S9 holds for b4 being strict non-empty MSAlgebra over S holds ( b4 = A Over S iff ( the Sorts of b4 = the Sorts of A | the carrier of S & the Charact of b4 = the Charact of A | the carrier' of S ) ); theorem Th9: :: MSUHOM_1:9 for S being non empty non void strict ManySortedSign for A being strict non-empty MSAlgebra over S holds A = A Over S proof let S be non empty non void strict ManySortedSign ; ::_thesis: for A being strict non-empty MSAlgebra over S holds A = A Over S let A be strict non-empty MSAlgebra over S; ::_thesis: A = A Over S A1: the Charact of (A Over S) = the Charact of A | the carrier' of S by Def2 .= the Charact of A ; the Sorts of (A Over S) = the Sorts of A | the carrier of S by Def2 .= the Sorts of A ; hence A = A Over S by A1; ::_thesis: verum end; theorem Th10: :: MSUHOM_1:10 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds MSSign U1 = MSSign U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies MSSign U1 = MSSign U2 ) assume A1: U1,U2 are_similar ; ::_thesis: MSSign U1 = MSSign U2 reconsider f = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2; A2: ( the carrier of (MSSign U1) = {0} & the Arity of (MSSign U1) = f ) by MSUALG_1:def_8; reconsider f = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2; A3: ( the Arity of (MSSign U2) = f & the ResultSort of (MSSign U2) = (dom (signature U2)) --> 0 ) by MSUALG_1:def_8; A4: ( the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 & the carrier of (MSSign U2) = {0} ) by MSUALG_1:def_8; A5: ( the carrier' of (MSSign U1) = dom (signature U1) & the carrier' of (MSSign U2) = dom (signature U2) ) by MSUALG_1:def_8; then the carrier' of (MSSign U1) = the carrier' of (MSSign U2) by A1, UNIALG_2:def_1; hence MSSign U1 = MSSign U2 by A1, A2, A4, A5, A3, UNIALG_2:def_1; ::_thesis: verum end; definition let U1, U2 be Universal_Algebra; let h be Function of U1,U2; assume A1: MSSign U1 = MSSign U2 ; func MSAlg h -> ManySortedFunction of (MSAlg U1),((MSAlg U2) Over (MSSign U1)) equals :Def3: :: MSUHOM_1:def 3 0 .--> h; coherence 0 .--> h is ManySortedFunction of (MSAlg U1),((MSAlg U2) Over (MSSign U1)) proof the carrier of (MSSign U2) = {0} by MSUALG_1:def_8; then reconsider Z2 = the Sorts of (MSAlg U2) as ManySortedSet of {0} ; set f = 0 .--> h; MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; then A2: the Sorts of (MSAlg U2) . 0 = (0 .--> the carrier of U2) . 0 by MSUALG_1:def_9 .= the carrier of U2 by FUNCOP_1:72 ; A3: the carrier of (MSSign U1) = {0} by MSUALG_1:def_8; then reconsider Z1 = the Sorts of (MSAlg U1) as ManySortedSet of {0} ; MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; then A4: the Sorts of (MSAlg U1) . 0 = (0 .--> the carrier of U1) . 0 by MSUALG_1:def_9 .= the carrier of U1 by FUNCOP_1:72 ; now__::_thesis:_for_a_being_set_st_a_in_{0}_holds_ (0_.-->_h)_._a_is_Function_of_(_the_Sorts_of_(MSAlg_U1)_._a),(_the_Sorts_of_(MSAlg_U2)_._a) let a be set ; ::_thesis: ( a in {0} implies (0 .--> h) . a is Function of ( the Sorts of (MSAlg U1) . a),( the Sorts of (MSAlg U2) . a) ) assume a in {0} ; ::_thesis: (0 .--> h) . a is Function of ( the Sorts of (MSAlg U1) . a),( the Sorts of (MSAlg U2) . a) then a = 0 by TARSKI:def_1; hence (0 .--> h) . a is Function of ( the Sorts of (MSAlg U1) . a),( the Sorts of (MSAlg U2) . a) by A4, A2, FUNCOP_1:72; ::_thesis: verum end; then 0 .--> h is ManySortedFunction of Z1,Z2 by PBOOLE:def_15; hence 0 .--> h is ManySortedFunction of (MSAlg U1),((MSAlg U2) Over (MSSign U1)) by A1, A3, Th9; ::_thesis: verum end; end; :: deftheorem Def3 defines MSAlg MSUHOM_1:def_3_:_ for U1, U2 being Universal_Algebra for h being Function of U1,U2 st MSSign U1 = MSSign U2 holds MSAlg h = 0 .--> h; theorem Th11: :: MSUHOM_1:11 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st U1,U2 are_similar holds for o being OperSymbol of (MSSign U1) holds (MSAlg h) . (the_result_sort_of o) = h proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st U1,U2 are_similar holds for o being OperSymbol of (MSSign U1) holds (MSAlg h) . (the_result_sort_of o) = h let h be Function of U1,U2; ::_thesis: ( U1,U2 are_similar implies for o being OperSymbol of (MSSign U1) holds (MSAlg h) . (the_result_sort_of o) = h ) assume A1: U1,U2 are_similar ; ::_thesis: for o being OperSymbol of (MSSign U1) holds (MSAlg h) . (the_result_sort_of o) = h set f = MSAlg h; let o be OperSymbol of (MSSign U1); ::_thesis: (MSAlg h) . (the_result_sort_of o) = h A2: ( the carrier' of (MSSign U1) = dom (signature U1) & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 ) by MSUALG_1:def_8; A3: 0 in {0} by TARSKI:def_1; consider n being Nat such that A4: the carrier' of (MSSign U1) = Seg n by MSUALG_1:def_7; A5: (n |-> 0) . o = 0 by A4, FUNCOP_1:7; thus (MSAlg h) . (the_result_sort_of o) = (MSAlg h) . ( the ResultSort of (MSSign U1) . o) by MSUALG_1:def_2 .= (0 .--> h) . 0 by A1, A2, A4, A5, Def3, Th10 .= h by A3, FUNCOP_1:7 ; ::_thesis: verum end; theorem Th12: :: MSUHOM_1:12 for U1 being Universal_Algebra for o being OperSymbol of (MSSign U1) holds Den (o,(MSAlg U1)) = the charact of U1 . o proof let U1 be Universal_Algebra; ::_thesis: for o being OperSymbol of (MSSign U1) holds Den (o,(MSAlg U1)) = the charact of U1 . o let o be OperSymbol of (MSSign U1); ::_thesis: Den (o,(MSAlg U1)) = the charact of U1 . o MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; hence Den (o,(MSAlg U1)) = (MSCharact U1) . o by MSUALG_1:def_6 .= the charact of U1 . o by MSUALG_1:def_10 ; ::_thesis: verum end; Lm1: for U1 being Universal_Algebra holds dom (signature U1) = dom the charact of U1 proof let U1 be Universal_Algebra; ::_thesis: dom (signature U1) = dom the charact of U1 thus dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3 .= Seg (len the charact of U1) by UNIALG_1:def_4 .= dom the charact of U1 by FINSEQ_1:def_3 ; ::_thesis: verum end; theorem Th13: :: MSUHOM_1:13 for U1 being Universal_Algebra for o being OperSymbol of (MSSign U1) holds Den (o,(MSAlg U1)) is operation of U1 proof let U1 be Universal_Algebra; ::_thesis: for o being OperSymbol of (MSSign U1) holds Den (o,(MSAlg U1)) is operation of U1 let o be OperSymbol of (MSSign U1); ::_thesis: Den (o,(MSAlg U1)) is operation of U1 A1: dom (signature U1) = dom the charact of U1 by Lm1; ( Den (o,(MSAlg U1)) = the charact of U1 . o & the carrier' of (MSSign U1) = dom (signature U1) ) by Th12, MSUALG_1:def_8; hence Den (o,(MSAlg U1)) is operation of U1 by A1, FUNCT_1:def_3; ::_thesis: verum end; Lm2: for U1, U2 being Universal_Algebra st U1,U2 are_similar holds for o being OperSymbol of (MSSign U1) holds Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2 proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies for o being OperSymbol of (MSSign U1) holds Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2 ) set A = (MSAlg U2) Over (MSSign U1); A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; assume A2: U1,U2 are_similar ; ::_thesis: for o being OperSymbol of (MSSign U1) holds Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2 then A3: MSSign U1 = MSSign U2 by Th10; let o be OperSymbol of (MSSign U1); ::_thesis: Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2 A4: Den (o,((MSAlg U2) Over (MSSign U1))) = the Charact of ((MSAlg U2) Over (MSSign U1)) . o by MSUALG_1:def_6 .= (MSCharact U2) . o by A3, A1, Th9 .= the charact of U2 . o by MSUALG_1:def_10 ; A5: dom (signature U1) = dom the charact of U1 by Lm1; signature U1 = signature U2 by A2, UNIALG_2:def_1; then ( the carrier' of (MSSign U1) = dom (signature U1) & dom the charact of U1 = dom the charact of U2 ) by A5, Lm1, MSUALG_1:def_8; hence Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2 by A4, A5, FUNCT_1:def_3; ::_thesis: verum end; theorem Th14: :: MSUHOM_1:14 for U1 being Universal_Algebra for o being OperSymbol of (MSSign U1) for y being Element of Args (o,(MSAlg U1)) holds y is FinSequence of the carrier of U1 proof let U1 be Universal_Algebra; ::_thesis: for o being OperSymbol of (MSSign U1) for y being Element of Args (o,(MSAlg U1)) holds y is FinSequence of the carrier of U1 let o be OperSymbol of (MSSign U1); ::_thesis: for y being Element of Args (o,(MSAlg U1)) holds y is FinSequence of the carrier of U1 let y be Element of Args (o,(MSAlg U1)); ::_thesis: y is FinSequence of the carrier of U1 set O1 = Den (o,(MSAlg U1)); A1: ( Den (o,(MSAlg U1)) = the charact of U1 . o & the carrier' of (MSSign U1) = dom (signature U1) ) by Th12, MSUALG_1:def_8; dom (signature U1) = dom the charact of U1 by Lm1; then reconsider O1 = Den (o,(MSAlg U1)) as operation of U1 by A1, FUNCT_1:def_3; Args (o,(MSAlg U1)) = dom O1 by FUNCT_2:def_1; then y in the carrier of U1 * by TARSKI:def_3; hence y is FinSequence of the carrier of U1 by FINSEQ_1:def_11; ::_thesis: verum end; theorem Th15: :: MSUHOM_1:15 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st U1,U2 are_similar holds for o being OperSymbol of (MSSign U1) for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st U1,U2 are_similar holds for o being OperSymbol of (MSSign U1) for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y let h be Function of U1,U2; ::_thesis: ( U1,U2 are_similar implies for o being OperSymbol of (MSSign U1) for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y ) assume A1: U1,U2 are_similar ; ::_thesis: for o being OperSymbol of (MSSign U1) for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y reconsider f1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2; let o be OperSymbol of (MSSign U1); ::_thesis: for y being Element of Args (o,(MSAlg U1)) holds (MSAlg h) # y = h * y A2: the carrier' of (MSSign U2) = dom (signature U2) by MSUALG_1:def_8; MSSign U1 = MSSign U2 by A1, Th10; then o in dom (signature U2) by A2; then A3: o in dom (signature U1) by A1, UNIALG_2:def_1; then o in dom f1 by FUNCT_2:def_1; then A4: ((*--> 0) * (signature U1)) . o = (*--> 0) . ((signature U1) . o) by FUNCT_1:12; let y be Element of Args (o,(MSAlg U1)); ::_thesis: (MSAlg h) # y = h * y set f = MSAlg h; A5: the carrier of (MSSign U1) = {0} by MSUALG_1:def_8; set X = dom (h * y); A6: dom h = the carrier of U1 by FUNCT_2:def_1; A7: y is FinSequence of the carrier of U1 by Th14; then rng y c= the carrier of U1 by FINSEQ_1:def_4; then reconsider p = h * y as FinSequence by A7, A6, FINSEQ_1:16; A8: dom (h * y) = dom y by A7, FINSEQ_3:120; the Arity of (MSSign U1) = f1 by MSUALG_1:def_8; then A9: the_arity_of o = ((*--> 0) * (signature U1)) . o by MSUALG_1:def_1; (signature U1) . o in rng (signature U1) by A3, FUNCT_1:def_3; then consider n being Element of NAT such that A10: n = (signature U1) . o ; A11: 0 in {0} by TARSKI:def_1; A12: now__::_thesis:_for_m_being_Nat_st_m_in_dom_y_holds_ (MSAlg_h)_._((the_arity_of_o)_/._m)_=_h 0 is Element of {0} by TARSKI:def_1; then n |-> 0 is FinSequence of {0} by FINSEQ_2:63; then reconsider l = n |-> 0 as Element of the carrier of (MSSign U1) * by A5, FINSEQ_1:def_11; let m be Nat; ::_thesis: ( m in dom y implies (MSAlg h) . ((the_arity_of o) /. m) = h ) A13: ( (the_arity_of o) /. m = l /. m & dom (n |-> 0) = Seg n ) by A9, A4, A10, FINSEQ_2:def_6, FUNCOP_1:13; assume m in dom y ; ::_thesis: (MSAlg h) . ((the_arity_of o) /. m) = h then m in dom (the_arity_of o) by MSUALG_3:6; then A14: m in dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def_6; then l /. m = l . m by PARTFUN1:def_6; then (the_arity_of o) /. m = 0 by A14, A13, FUNCOP_1:7; hence (MSAlg h) . ((the_arity_of o) /. m) = (0 .--> h) . 0 by A1, Def3, Th10 .= h by A11, FUNCOP_1:7 ; ::_thesis: verum end; A15: now__::_thesis:_for_m_being_Nat_st_m_in_dom_y_holds_ ((MSAlg_h)_#_y)_._m_=_p_._m let m be Nat; ::_thesis: ( m in dom y implies ((MSAlg h) # y) . m = p . m ) assume A16: m in dom y ; ::_thesis: ((MSAlg h) # y) . m = p . m then A17: m in dom (h * y) by A7, FINSEQ_3:120; ((MSAlg h) # y) . m = ((MSAlg h) . ((the_arity_of o) /. m)) . (y . m) by A16, MSUALG_3:def_6; hence ((MSAlg h) # y) . m = h . (y . m) by A12, A16 .= p . m by A7, A17, FINSEQ_3:120 ; ::_thesis: verum end; dom ((MSAlg h) # y) = dom (the_arity_of o) by MSUALG_3:6 .= dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def_6 .= Seg n by FUNCOP_1:13 ; then A18: (MSAlg h) # y is FinSequence by FINSEQ_1:def_2; A19: dom y = dom (the_arity_of o) by MSUALG_3:6 .= dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def_6 .= Seg n by FUNCOP_1:13 ; dom ((MSAlg h) # y) = dom (the_arity_of o) by MSUALG_3:6 .= dom (n |-> 0) by A9, A4, A10, FINSEQ_2:def_6 .= Seg n by FUNCOP_1:13 .= dom (h * y) by A7, A19, FINSEQ_3:120 ; hence (MSAlg h) # y = h * y by A18, A15, A8, FINSEQ_1:13; ::_thesis: verum end; theorem Th16: :: MSUHOM_1:16 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st h is_homomorphism U1,U2 holds MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st h is_homomorphism U1,U2 holds MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) let h be Function of U1,U2; ::_thesis: ( h is_homomorphism U1,U2 implies MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ) set f = MSAlg h; set A = (MSAlg U2) Over (MSSign U1); A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; consider m being Nat such that A2: the carrier' of (MSSign U1) = Seg m by MSUALG_1:def_7; assume A3: h is_homomorphism U1,U2 ; ::_thesis: MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) then A4: U1,U2 are_similar by ALG_1:def_1; then A5: MSSign U1 = MSSign U2 by Th10; let o be OperSymbol of (MSSign U1); :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(MSAlg U1)) = {} or for b1 being Element of Args (o,(MSAlg U1)) holds ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . b1) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # b1) ) assume Args (o,(MSAlg U1)) <> {} ; ::_thesis: for b1 being Element of Args (o,(MSAlg U1)) holds ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . b1) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # b1) o in Seg m by A2; then reconsider k = o as Element of NAT ; reconsider O2 = Den (o,((MSAlg U2) Over (MSSign U1))) as operation of U2 by A4, Lm2; Den (o,((MSAlg U2) Over (MSSign U1))) = the Charact of ((MSAlg U2) Over (MSSign U1)) . o by MSUALG_1:def_6 .= (MSCharact U2) . o by A5, A1, Th9 .= the charact of U2 . o by MSUALG_1:def_10 ; then A6: O2 = the charact of U2 . k ; set O1 = Den (o,(MSAlg U1)); let y be Element of Args (o,(MSAlg U1)); ::_thesis: ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y) A7: ( Den (o,(MSAlg U1)) = the charact of U1 . o & the carrier' of (MSSign U1) = dom (signature U1) ) by Th12, MSUALG_1:def_8; reconsider O1 = Den (o,(MSAlg U1)) as operation of U1 by Th13; A8: y is FinSequence of the carrier of U1 by Th14; ( dom (signature U1) = dom the charact of U1 & Args (o,(MSAlg U1)) = dom O1 ) by Lm1, FUNCT_2:def_1; then h . (O1 . y) = O2 . (h * y) by A3, A7, A6, A8, ALG_1:def_1 .= (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y) by A4, Th15 ; hence ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y) by A4, Th11; ::_thesis: verum end; Lm3: for U1 being Universal_Algebra for n being Nat st n in dom the charact of U1 holds n is OperSymbol of (MSSign U1) proof let U1 be Universal_Algebra; ::_thesis: for n being Nat st n in dom the charact of U1 holds n is OperSymbol of (MSSign U1) A1: dom (signature U1) = dom the charact of U1 by Lm1; let n be Nat; ::_thesis: ( n in dom the charact of U1 implies n is OperSymbol of (MSSign U1) ) assume n in dom the charact of U1 ; ::_thesis: n is OperSymbol of (MSSign U1) hence n is OperSymbol of (MSSign U1) by A1, MSUALG_1:def_8; ::_thesis: verum end; theorem Th17: :: MSUHOM_1:17 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st U1,U2 are_similar holds MSAlg h is ManySortedSet of {0} proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st U1,U2 are_similar holds MSAlg h is ManySortedSet of {0} let h be Function of U1,U2; ::_thesis: ( U1,U2 are_similar implies MSAlg h is ManySortedSet of {0} ) assume U1,U2 are_similar ; ::_thesis: MSAlg h is ManySortedSet of {0} then MSAlg h = 0 .--> h by Def3, Th10; hence MSAlg h is ManySortedSet of {0} ; ::_thesis: verum end; theorem Th18: :: MSUHOM_1:18 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st h is_epimorphism U1,U2 holds MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st h is_epimorphism U1,U2 holds MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) let h be Function of U1,U2; ::_thesis: ( h is_epimorphism U1,U2 implies MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ) set f = MSAlg h; set A = (MSAlg U2) Over (MSSign U1); A1: 0 in {0} by TARSKI:def_1; MSSorts U2 = 0 .--> the carrier of U2 by MSUALG_1:def_9; then A2: ( the carrier of (MSSign U1) = {0} & (MSSorts U2) . 0 = the carrier of U2 ) by A1, FUNCOP_1:7, MSUALG_1:def_8; A3: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; assume A4: h is_epimorphism U1,U2 ; ::_thesis: MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) then A5: rng h = the carrier of U2 by ALG_1:def_3; A6: h is_homomorphism U1,U2 by A4, ALG_1:def_3; then A7: U1,U2 are_similar by ALG_1:def_1; then MSSign U1 = MSSign U2 by Th10; then A8: the Sorts of ((MSAlg U2) Over (MSSign U1)) = MSSorts U2 by A3, Th9; thus MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A6, Th16; :: according to MSUALG_3:def_8 ::_thesis: MSAlg h is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in the carrier of (MSSign U1) or rng ((MSAlg h) . i) = the Sorts of ((MSAlg U2) Over (MSSign U1)) . i ) assume i in the carrier of (MSSign U1) ; ::_thesis: rng ((MSAlg h) . i) = the Sorts of ((MSAlg U2) Over (MSSign U1)) . i then reconsider i9 = i as Element of (MSSign U1) ; reconsider h9 = (MSAlg h) . i as Function of ( the Sorts of (MSAlg U1) . i9),( the Sorts of ((MSAlg U2) Over (MSSign U1)) . i9) by PBOOLE:def_15; (MSAlg h) . 0 = (0 .--> h) . 0 by A7, Def3, Th10 .= h by A1, FUNCOP_1:7 ; then ( the carrier of (MSSign U1) = {0} & rng h9 = the Sorts of ((MSAlg U2) Over (MSSign U1)) . 0 ) by A5, A8, A2, TARSKI:def_1; hence rng ((MSAlg h) . i) = the Sorts of ((MSAlg U2) Over (MSSign U1)) . i by TARSKI:def_1; ::_thesis: verum end; theorem Th19: :: MSUHOM_1:19 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st h is_monomorphism U1,U2 holds MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st h is_monomorphism U1,U2 holds MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) let h be Function of U1,U2; ::_thesis: ( h is_monomorphism U1,U2 implies MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ) set f = MSAlg h; the carrier of (MSSign U1) = {0} by MSUALG_1:def_8; then A1: dom (MSAlg h) = {0} by PARTFUN1:def_2; assume A2: h is_monomorphism U1,U2 ; ::_thesis: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) then A3: h is_homomorphism U1,U2 by ALG_1:def_2; hence MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by Th16; :: according to MSUALG_3:def_9 ::_thesis: MSAlg h is "1-1" U1,U2 are_similar by A3, ALG_1:def_1; then MSAlg h = 0 .--> h by Def3, Th10; then A4: (MSAlg h) . 0 = h by FUNCOP_1:72; let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds ( not i in dom (MSAlg h) or not (MSAlg h) . i = b1 or b1 is one-to-one ) let h9 be Function; ::_thesis: ( not i in dom (MSAlg h) or not (MSAlg h) . i = h9 or h9 is one-to-one ) assume ( i in dom (MSAlg h) & (MSAlg h) . i = h9 ) ; ::_thesis: h9 is one-to-one then h = h9 by A4, A1, TARSKI:def_1; hence h9 is one-to-one by A2, ALG_1:def_2; ::_thesis: verum end; theorem :: MSUHOM_1:20 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st h is_isomorphism U1,U2 holds MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st h is_isomorphism U1,U2 holds MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) let h be Function of U1,U2; ::_thesis: ( h is_isomorphism U1,U2 implies MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ) set A = (MSAlg U2) Over (MSSign U1); set f = MSAlg h; assume A1: h is_isomorphism U1,U2 ; ::_thesis: MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) then h is_epimorphism U1,U2 by ALG_1:def_4; hence MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by Th18; :: according to MSUALG_3:def_10 ::_thesis: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) h is_monomorphism U1,U2 by A1, ALG_1:def_4; hence MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by Th19; ::_thesis: verum end; theorem Th21: :: MSUHOM_1:21 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_homomorphism U1,U2 proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_homomorphism U1,U2 let h be Function of U1,U2; ::_thesis: ( U1,U2 are_similar & MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_homomorphism U1,U2 ) assume A1: U1,U2 are_similar ; ::_thesis: ( not MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_homomorphism U1,U2 ) A2: MSSign U1 = MSSign U2 by A1, Th10; set A = (MSAlg U2) Over (MSSign U1); set f = MSAlg h; assume A3: MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ; ::_thesis: h is_homomorphism U1,U2 thus U1,U2 are_similar by A1; :: according to ALG_1:def_1 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom the charact of U1 or for b2 being M16( the carrier of U1, Operations U1) for b3 being M16( the carrier of U2, Operations U2) holds ( not b2 = the charact of U1 . b1 or not b3 = the charact of U2 . b1 or for b4 being FinSequence of the carrier of U1 holds ( not b4 in dom b2 or h . (b2 . b4) = b3 . K141( the carrier of U1, the carrier of U2,b4,h) ) ) ) let n be Element of NAT ; ::_thesis: ( not n in dom the charact of U1 or for b1 being M16( the carrier of U1, Operations U1) for b2 being M16( the carrier of U2, Operations U2) holds ( not b1 = the charact of U1 . n or not b2 = the charact of U2 . n or for b3 being FinSequence of the carrier of U1 holds ( not b3 in dom b1 or h . (b1 . b3) = b2 . K141( the carrier of U1, the carrier of U2,b3,h) ) ) ) assume n in dom the charact of U1 ; ::_thesis: for b1 being M16( the carrier of U1, Operations U1) for b2 being M16( the carrier of U2, Operations U2) holds ( not b1 = the charact of U1 . n or not b2 = the charact of U2 . n or for b3 being FinSequence of the carrier of U1 holds ( not b3 in dom b1 or h . (b1 . b3) = b2 . K141( the carrier of U1, the carrier of U2,b3,h) ) ) then reconsider o = n as OperSymbol of (MSSign U1) by Lm3; let O1 be operation of U1; ::_thesis: for b1 being M16( the carrier of U2, Operations U2) holds ( not O1 = the charact of U1 . n or not b1 = the charact of U2 . n or for b2 being FinSequence of the carrier of U1 holds ( not b2 in dom O1 or h . (O1 . b2) = b1 . K141( the carrier of U1, the carrier of U2,b2,h) ) ) let O2 be operation of U2; ::_thesis: ( not O1 = the charact of U1 . n or not O2 = the charact of U2 . n or for b1 being FinSequence of the carrier of U1 holds ( not b1 in dom O1 or h . (O1 . b1) = O2 . K141( the carrier of U1, the carrier of U2,b1,h) ) ) assume that A4: O1 = the charact of U1 . n and A5: O2 = the charact of U2 . n ; ::_thesis: for b1 being FinSequence of the carrier of U1 holds ( not b1 in dom O1 or h . (O1 . b1) = O2 . K141( the carrier of U1, the carrier of U2,b1,h) ) A6: O1 = Den (o,(MSAlg U1)) by A4, Th12; let x be FinSequence of U1; ::_thesis: ( not x in dom O1 or h . (O1 . x) = O2 . K141( the carrier of U1, the carrier of U2,x,h) ) assume x in dom O1 ; ::_thesis: h . (O1 . x) = O2 . K141( the carrier of U1, the carrier of U2,x,h) then reconsider y = x as Element of Args (o,(MSAlg U1)) by A6, FUNCT_2:def_1; A7: ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = h . (O1 . y) by A1, A6, Th11; A8: ((MSAlg h) . (the_result_sort_of o)) . ((Den (o,(MSAlg U1))) . y) = (Den (o,((MSAlg U2) Over (MSSign U1)))) . ((MSAlg h) # y) by A3, MSUALG_3:def_7; A9: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def_11; Den (o,((MSAlg U2) Over (MSSign U1))) = the Charact of ((MSAlg U2) Over (MSSign U1)) . o by MSUALG_1:def_6 .= (MSCharact U2) . o by A2, A9, Th9 .= O2 by A5, MSUALG_1:def_10 ; hence h . (O1 . x) = O2 . K141( the carrier of U1, the carrier of U2,x,h) by A1, A7, A8, Th15; ::_thesis: verum end; theorem Th22: :: MSUHOM_1:22 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_epimorphism U1,U2 proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_epimorphism U1,U2 let h be Function of U1,U2; ::_thesis: ( U1,U2 are_similar & MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_epimorphism U1,U2 ) set B = the Sorts of ((MSAlg U2) Over (MSSign U1)); set I = the carrier of (MSSign U1); A1: 0 in {0} by TARSKI:def_1; MSSorts U2 = 0 .--> the carrier of U2 by MSUALG_1:def_9; then A2: (MSSorts U2) . 0 = the carrier of U2 by A1, FUNCOP_1:7; A3: ( the carrier of (MSSign U1) = {0} & MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) ) by MSUALG_1:def_8, MSUALG_1:def_11; assume A4: U1,U2 are_similar ; ::_thesis: ( not MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_epimorphism U1,U2 ) then MSSign U1 = MSSign U2 by Th10; then A5: the Sorts of ((MSAlg U2) Over (MSSign U1)) = the Sorts of (MSAlg U2) by Th9; assume A6: MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ; ::_thesis: h is_epimorphism U1,U2 then A7: MSAlg h is "onto" by MSUALG_3:def_8; MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A6, MSUALG_3:def_8; then A8: h is_homomorphism U1,U2 by A4, Th21; (MSAlg h) . 0 = (0 .--> h) . 0 by A4, Def3, Th10 .= h by A1, FUNCOP_1:7 ; then rng h = the carrier of U2 by A7, A1, A2, A5, A3, MSUALG_3:def_3; hence h is_epimorphism U1,U2 by A8, ALG_1:def_3; ::_thesis: verum end; theorem Th23: :: MSUHOM_1:23 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_monomorphism U1,U2 proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_monomorphism U1,U2 let h be Function of U1,U2; ::_thesis: ( U1,U2 are_similar & MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_monomorphism U1,U2 ) assume A1: U1,U2 are_similar ; ::_thesis: ( not MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_monomorphism U1,U2 ) assume A2: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ; ::_thesis: h is_monomorphism U1,U2 then A3: MSAlg h is "1-1" by MSUALG_3:def_9; MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A2, MSUALG_3:def_9; then A4: h is_homomorphism U1,U2 by A1, Th21; A5: the carrier of (MSSign U1) = {0} by MSUALG_1:def_8; A6: 0 in {0} by TARSKI:def_1; (MSAlg h) . 0 = (0 .--> h) . 0 by A1, Def3, Th10 .= h by A6, FUNCOP_1:7 ; then h is one-to-one by A3, A5, A6, MSUALG_3:1; hence h is_monomorphism U1,U2 by A4, ALG_1:def_2; ::_thesis: verum end; theorem :: MSUHOM_1:24 for U1, U2 being Universal_Algebra for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_isomorphism U1,U2 proof let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds h is_isomorphism U1,U2 let h be Function of U1,U2; ::_thesis: ( U1,U2 are_similar & MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_isomorphism U1,U2 ) assume A1: U1,U2 are_similar ; ::_thesis: ( not MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_isomorphism U1,U2 ) assume A2: MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ; ::_thesis: h is_isomorphism U1,U2 then MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by MSUALG_3:def_10; hence h is_monomorphism U1,U2 by A1, Th23; :: according to ALG_1:def_4 ::_thesis: h is_epimorphism U1,U2 MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A2, MSUALG_3:def_10; hence h is_epimorphism U1,U2 by A1, Th22; ::_thesis: verum end; theorem :: MSUHOM_1:25 for U1 being Universal_Algebra holds MSAlg (id the carrier of U1) = id the Sorts of (MSAlg U1) proof let U1 be Universal_Algebra; ::_thesis: MSAlg (id the carrier of U1) = id the Sorts of (MSAlg U1) set f = id the Sorts of (MSAlg U1); set h = id the carrier of U1; A1: the carrier of (MSSign U1) = {0} by MSUALG_1:def_8; then reconsider Z1 = the Sorts of (MSAlg U1) as ManySortedSet of {0} ; A2: now__::_thesis:_for_i_being_set_st_i_in_{0}_holds_ (id_the_Sorts_of_(MSAlg_U1))_._0_=_id_the_carrier_of_U1 let i be set ; ::_thesis: ( i in {0} implies (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1 ) MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def_11; then A3: Z1 . 0 = (0 .--> the carrier of U1) . 0 by MSUALG_1:def_9 .= the carrier of U1 by FUNCOP_1:72 ; assume A4: i in {0} ; ::_thesis: (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1 then i = 0 by TARSKI:def_1; hence (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1 by A1, A4, A3, MSUALG_3:def_1; ::_thesis: verum end; MSAlg (id the carrier of U1) = 0 .--> (id the carrier of U1) by Def3; then A5: (MSAlg (id the carrier of U1)) . 0 = id the carrier of U1 by FUNCOP_1:72; now__::_thesis:_for_a_being_set_st_a_in_{0}_holds_ (id_the_Sorts_of_(MSAlg_U1))_._a_=_(MSAlg_(id_the_carrier_of_U1))_._a let a be set ; ::_thesis: ( a in {0} implies (id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a ) assume A6: a in {0} ; ::_thesis: (id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a then a = 0 by TARSKI:def_1; hence (id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a by A2, A5, A6; ::_thesis: verum end; hence id the Sorts of (MSAlg U1) = MSAlg (id the carrier of U1) by A1, PBOOLE:3; ::_thesis: verum end; theorem :: MSUHOM_1:26 for U1, U2, U3 being Universal_Algebra st U1,U2 are_similar & U2,U3 are_similar holds for h1 being Function of U1,U2 for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) proof let U1, U2, U3 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar & U2,U3 are_similar implies for h1 being Function of U1,U2 for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) ) assume that A1: U1,U2 are_similar and A2: U2,U3 are_similar ; ::_thesis: for h1 being Function of U1,U2 for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) let h1 be Function of U1,U2; ::_thesis: for h2 being Function of U2,U3 holds (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) let h2 be Function of U2,U3; ::_thesis: (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) A3: MSAlg h1 is ManySortedSet of {0} by A1, Th17; MSAlg h2 is ManySortedSet of {0} by A2, Th17; then A4: dom (MSAlg h2) = {0} by PARTFUN1:def_2; A5: dom ((MSAlg h2) ** (MSAlg h1)) = (dom (MSAlg h1)) /\ (dom (MSAlg h2)) by PBOOLE:def_19 .= {0} /\ {0} by A3, A4, PARTFUN1:def_2 .= {0} ; A6: now__::_thesis:_for_a_being_set_ for_f,_g_being_Function_st_a_in_dom_((MSAlg_h2)_**_(MSAlg_h1))_&_f_=_(MSAlg_h1)_._a_&_g_=_(MSAlg_h2)_._a_holds_ ((MSAlg_h2)_**_(MSAlg_h1))_._a_=_h2_*_h1 let a be set ; ::_thesis: for f, g being Function st a in dom ((MSAlg h2) ** (MSAlg h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a holds ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1 let f, g be Function; ::_thesis: ( a in dom ((MSAlg h2) ** (MSAlg h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a implies ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1 ) assume that A7: a in dom ((MSAlg h2) ** (MSAlg h1)) and A8: f = (MSAlg h1) . a and A9: g = (MSAlg h2) . a ; ::_thesis: ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1 A10: g = (MSAlg h2) . 0 by A5, A7, A9, TARSKI:def_1 .= (0 .--> h2) . 0 by A2, Def3, Th10 .= h2 by FUNCOP_1:72 ; f = (MSAlg h1) . 0 by A5, A7, A8, TARSKI:def_1 .= (0 .--> h1) . 0 by A1, Def3, Th10 .= h1 by FUNCOP_1:72 ; hence ((MSAlg h2) ** (MSAlg h1)) . a = h2 * h1 by A7, A8, A9, A10, PBOOLE:def_19; ::_thesis: verum end; set h = h2 * h1; A11: MSAlg (h2 * h1) is ManySortedSet of {0} by A1, A2, Th17, UNIALG_2:2; A12: MSSign U2 = MSSign U3 by A2, Th10; A13: now__::_thesis:_for_a_being_set_st_a_in_dom_(MSAlg_(h2_*_h1))_holds_ (MSAlg_(h2_*_h1))_._a_=_h2_*_h1 let a be set ; ::_thesis: ( a in dom (MSAlg (h2 * h1)) implies (MSAlg (h2 * h1)) . a = h2 * h1 ) assume a in dom (MSAlg (h2 * h1)) ; ::_thesis: (MSAlg (h2 * h1)) . a = h2 * h1 then A14: a in {0} by A11, PARTFUN1:def_2; (MSAlg (h2 * h1)) . 0 = (0 .--> (h2 * h1)) . 0 by A1, A12, Def3, Th10 .= h2 * h1 by FUNCOP_1:72 ; hence (MSAlg (h2 * h1)) . a = h2 * h1 by A14, TARSKI:def_1; ::_thesis: verum end; A15: dom (MSAlg (h2 * h1)) = {0} by A11, PARTFUN1:def_2; A16: now__::_thesis:_for_a_being_set_ for_f,_g_being_Function_st_a_in_dom_(MSAlg_(h2_*_h1))_&_f_=_(MSAlg_h1)_._a_&_g_=_(MSAlg_h2)_._a_holds_ (MSAlg_(h2_*_h1))_._a_=_((MSAlg_h2)_**_(MSAlg_h1))_._a let a be set ; ::_thesis: for f, g being Function st a in dom (MSAlg (h2 * h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a holds (MSAlg (h2 * h1)) . a = ((MSAlg h2) ** (MSAlg h1)) . a let f, g be Function; ::_thesis: ( a in dom (MSAlg (h2 * h1)) & f = (MSAlg h1) . a & g = (MSAlg h2) . a implies (MSAlg (h2 * h1)) . a = ((MSAlg h2) ** (MSAlg h1)) . a ) assume that A17: a in dom (MSAlg (h2 * h1)) and A18: ( f = (MSAlg h1) . a & g = (MSAlg h2) . a ) ; ::_thesis: (MSAlg (h2 * h1)) . a = ((MSAlg h2) ** (MSAlg h1)) . a thus (MSAlg (h2 * h1)) . a = h2 * h1 by A13, A17 .= ((MSAlg h2) ** (MSAlg h1)) . a by A5, A6, A15, A17, A18 ; ::_thesis: verum end; A19: dom (MSAlg (h2 * h1)) = {0} by A11, PARTFUN1:def_2; A20: for a being set st a in {0} holds ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a proof let a be set ; ::_thesis: ( a in {0} implies ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a ) A21: ( (MSAlg h1) . a is Function & (MSAlg h2) . a is Function ) ; assume a in {0} ; ::_thesis: ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a hence ((MSAlg h2) ** (MSAlg h1)) . a = (MSAlg (h2 * h1)) . a by A19, A16, A21; ::_thesis: verum end; (MSAlg h2) ** (MSAlg h1) is ManySortedSet of {0} by A5, PARTFUN1:def_2, RELAT_1:def_18; hence (MSAlg h2) ** (MSAlg h1) = MSAlg (h2 * h1) by A11, A20, PBOOLE:3; ::_thesis: verum end;