:: 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;