:: MSUALG_4 semantic presentation

begin


registration
let I be set ;
cluster Relation-like I -defined Function-like total Relation-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is Relation-yielding
proof
set R = the Relation;
set f = I --> the Relation;
reconsider f = I --> the Relation as ManySortedSet of I ;
take  f ; ::_thesis: f is Relation-yielding
 for x being set st x in dom f holds
f . x is Relation by FUNCOP_1:7;
hence  f is Relation-yielding by FUNCOP_1:def_11; ::_thesis: verum
end;
end;

definition
let I be set ;
let A, B be ManySortedSet of I;
mode ManySortedRelation of A,B ->  ManySortedSet of I means :Def1: :: MSUALG_4:def 1
 for i being set st i in I holds
it . i is Relation of (A . i),(B . i);
existence
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is Relation of (A . i),(B . i)
proof
consider R being Relation such that
A1: R = {} ;
set f = I --> R;
reconsider f = I --> R as ManySortedSet of I ;
take  f ; ::_thesis: for i being set st i in I holds
f . i is Relation of (A . i),(B . i)
 for i being set st i in I holds
f . i is Relation of (A . i),(B . i)
proof
let i be set ; ::_thesis: ( i in I implies f . i is Relation of (A . i),(B . i) )
assume  i in I ; ::_thesis: f . i is Relation of (A . i),(B . i)
then  f . i = {} by A1, FUNCOP_1:7;
hence  f . i is Relation of (A . i),(B . i) by RELSET_1:12; ::_thesis: verum
end;
hence  for i being set st i in I holds
f . i is Relation of (A . i),(B . i) ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines ManySortedRelation MSUALG_4:def_1_:_
 for I being set
for A, B, b4 being ManySortedSet of I holds
( b4 is ManySortedRelation of A,B iff for i being set st i in I holds
b4 . i is Relation of (A . i),(B . i) );

registration
let I be set ;
let A, B be ManySortedSet of I;
cluster  ->  Relation-yielding for ManySortedRelation of A,B;
coherence
 for b1 being ManySortedRelation of A,B holds b1 is Relation-yielding
proof
let R be ManySortedRelation of A,B; ::_thesis: R is Relation-yielding
let x be set ; :: according to FUNCOP_1:def_11 ::_thesis: ( not x in dom R or R . x is set )
assume  x in dom R ; ::_thesis: R . x is set
then  x in I ;
hence  R . x is set by Def1; ::_thesis: verum
end;
end;

definition
let I be set ;
let A be ManySortedSet of I;
mode ManySortedRelation of A is ManySortedRelation of A,A;
end;

definition
let I be set ;
let A be ManySortedSet of I;
let IT be ManySortedRelation of A;
attrIT is MSEquivalence_Relation-like  means :Def2: :: MSUALG_4:def 2
 for i being set
for R being Relation of (A . i) st i in I & IT . i = R holds
R is Equivalence_Relation of (A . i);
end;

:: deftheorem Def2 defines MSEquivalence_Relation-like MSUALG_4:def_2_:_
 for I being set
for A being ManySortedSet of I
for IT being ManySortedRelation of A holds
( IT is MSEquivalence_Relation-like iff for i being set
for R being Relation of (A . i) st i in I & IT . i = R holds
R is Equivalence_Relation of (A . i) );

definition
let I be non empty set ;
let A, B be ManySortedSet of I;
let F be ManySortedRelation of A,B;
let i be Element of I;
:: original: .
redefine funcF . i ->  Relation of (A . i),(B . i);
coherence
 F . i is Relation of (A . i),(B . i) by Def1;
end;

definition
let S be non empty ManySortedSign ;
let U1 be MSAlgebra over S;
mode ManySortedRelation of U1 is ManySortedRelation of the Sorts of U1;
end;

definition
let S be non empty ManySortedSign ;
let U1 be MSAlgebra over S;
let IT be ManySortedRelation of U1;
attrIT is MSEquivalence-like  means :Def3: :: MSUALG_4:def 3
IT is MSEquivalence_Relation-like ;
end;

:: deftheorem Def3 defines MSEquivalence-like MSUALG_4:def_3_:_
 for S being non empty ManySortedSign
for U1 being MSAlgebra over S
for IT being ManySortedRelation of U1 holds
( IT is MSEquivalence-like iff IT is MSEquivalence_Relation-like );

registration
let S be non empty non void ManySortedSign ;
let U1 be MSAlgebra over S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like for ManySortedRelation of the Sorts of U1, the Sorts of U1;
existence
 ex b1 being ManySortedRelation of U1 st b1 is MSEquivalence-like
proof
deffunc H1( Element of S) ->  Element of K10(K11(( the Sorts of U1 . S),( the Sorts of U1 . S))) = id ( the Sorts of U1 . S);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
 for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) )
assume  i in the carrier of S ; ::_thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then  f . i = id ( the Sorts of U1 . i) by A1;
hence  f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by Def1;
reconsider f = f as ManySortedRelation of U1 ;
take  f ; ::_thesis: f is MSEquivalence-like
 for i being set
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
let R be Relation of ( the Sorts of U1 . i); ::_thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) )
assume  ( i in the carrier of S & f . i = R ) ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
then  R = id ( the Sorts of U1 . i) by A1;
hence  R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum
end;
then  f is MSEquivalence_Relation-like by Def2;
hence  f is MSEquivalence-like by Def3; ::_thesis: verum
end;
end;

theorem Th1: :: MSUALG_4:1
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for s being SortSymbol of S
for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S
for s being SortSymbol of S
for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s)
let U1 be MSAlgebra over S; ::_thesis: for s being SortSymbol of S
for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s)
let s be SortSymbol of S; ::_thesis: for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s)
let R be MSEquivalence-like ManySortedRelation of U1; ::_thesis: R . s is Equivalence_Relation of ( the Sorts of U1 . s)
 R is MSEquivalence_Relation-like by Def3;
hence  R . s is Equivalence_Relation of ( the Sorts of U1 . s) by Def2; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSEquivalence-like ManySortedRelation of U1;
attrR is MSCongruence-like  means :Def4: :: MSUALG_4:def 4
 for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in R . (the_result_sort_of o);
end;

:: deftheorem Def4 defines MSCongruence-like MSUALG_4:def_4_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSEquivalence-like ManySortedRelation of U1 holds
( R is MSCongruence-like iff for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in R . (the_result_sort_of o) );

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like MSCongruence-like for ManySortedRelation of the Sorts of U1, the Sorts of U1;
existence
 ex b1 being MSEquivalence-like ManySortedRelation of U1 st b1 is MSCongruence-like
proof
deffunc H1( Element of S) ->  Element of K10(K11(( the Sorts of U1 . S),( the Sorts of U1 . S))) = id ( the Sorts of U1 . S);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
 for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) )
assume  i in the carrier of S ; ::_thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then  f . i = id ( the Sorts of U1 . i) by A1;
hence  f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedRelation of the Sorts of U1, the Sorts of U1 by Def1;
reconsider f = f as ManySortedRelation of U1 ;
 for i being set
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
let R be Relation of ( the Sorts of U1 . i); ::_thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) )
assume  ( i in the carrier of S & f . i = R ) ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
then  R = id ( the Sorts of U1 . i) by A1;
hence  R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum
end;
then  f is MSEquivalence_Relation-like by Def2;
then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by Def3;
take  f ; ::_thesis: f is MSCongruence-like
 for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
proof
A2: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then A3: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
let x, y be Element of Args (o,U1); ::_thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) implies [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) )
A4: dom x = dom (the_arity_of o) by MSUALG_3:6;
assume A5: for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
A6: for a being set st a in dom (the_arity_of o) holds
x . a = y . a
proof
set ao = the_arity_of o;
let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies x . a = y . a )
assume A7: a in dom (the_arity_of o) ; ::_thesis: x . a = y . a
then reconsider n = a as Nat by ORDINAL1:def_12;
 (the_arity_of o) . n in rng (the_arity_of o) by A7, FUNCT_1:def_3;
then A8: f . ((the_arity_of o) . n) = id ( the Sorts of U1 . ((the_arity_of o) . n)) by A1;
 (the_arity_of o) /. n = (the_arity_of o) . n by A7, PARTFUN1:def_6;
then  [(x . n),(y . n)] in f . ((the_arity_of o) . n) by A5, A4, A7;
hence  x . a = y . a by A8, RELAT_1:def_10; ::_thesis: verum
end;
set r = the_result_sort_of o;
A9: f . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) by A1;
A10: Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . o) by A2, A3, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
 dom y = dom (the_arity_of o) by MSUALG_3:6;
then  (Den (o,U1)) . x = (Den (o,U1)) . y by A4, A6, FUNCT_1:2;
hence  [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A9, A10, RELAT_1:def_10; ::_thesis: verum
end;
hence  f is MSCongruence-like by Def4; ::_thesis: verum
end;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
mode MSCongruence of U1 is MSEquivalence-like MSCongruence-like ManySortedRelation of U1;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be MSAlgebra over S;
let R be MSEquivalence-like ManySortedRelation of U1;
let i be Element of S;
:: original: .
redefine funcR . i ->  Equivalence_Relation of ( the Sorts of U1 . i);
coherence
 R . i is Equivalence_Relation of ( the Sorts of U1 . i) by Th1;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be MSAlgebra over S;
let R be MSEquivalence-like ManySortedRelation of U1;
let i be Element of S;
let x be Element of the Sorts of U1 . i;
func Class (R,x) ->  Subset of ( the Sorts of U1 . i) equals :: MSUALG_4:def 5
 Class ((R . i),x);
correctness
coherence
Class ((R . i),x) is Subset of ( the Sorts of U1 . i);
;
end;

:: deftheorem  defines Class MSUALG_4:def_5_:_
 for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for R being MSEquivalence-like ManySortedRelation of U1
for i being Element of S
for x being Element of the Sorts of U1 . i holds Class (R,x) = Class ((R . i),x);

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func Class R ->  V8() ManySortedSet of the carrier of S means :Def6: :: MSUALG_4:def 6
 for s being Element of S holds it . s = Class (R . s);
existence
 ex b1 being V8() ManySortedSet of the carrier of S st
for s being Element of S holds b1 . s = Class (R . s)
proof
deffunc H1( Element of S) ->  a_partition of the Sorts of U1 . $1 = Class (R . $1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
 for i being set st i in the carrier of S holds
not f . i is empty
proof
let i be set ; ::_thesis: ( i in the carrier of S implies not f . i is empty )
assume  i in the carrier of S ; ::_thesis: not f . i is empty
then reconsider s = i as Element of S ;
consider x being set  such that
A2: x in the Sorts of U1 . s by XBOOLE_0:def_1;
reconsider y = x as Element of the Sorts of U1 . s by A2;
 f . s = Class (R . s) by A1;
then  Class ((R . s),y) in f . s by EQREL_1:def_3;
hence  not f . i is empty ; ::_thesis: verum
end;
then reconsider f = f as V8() ManySortedSet of the carrier of S by PBOOLE:def_13;
take  f ; ::_thesis: for s being Element of S holds f . s = Class (R . s)
thus  for s being Element of S holds f . s = Class (R . s) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being V8() ManySortedSet of the carrier of S st ( for s being Element of S holds b1 . s = Class (R . s) ) & ( for s being Element of S holds b2 . s = Class (R . s) ) holds
b1 = b2
proof
let C, D be V8() ManySortedSet of the carrier of S; ::_thesis: ( ( for s being Element of S holds C . s = Class (R . s) ) & ( for s being Element of S holds D . s = Class (R . s) ) implies C = D )
assume that
A3: for s being Element of S holds C . s = Class (R . s) and
A4: for s being Element of S holds D . s = Class (R . s) ; ::_thesis: C = D
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
C_._i_=_D_._i
let i be set ; ::_thesis: ( i in the carrier of S implies C . i = D . i )
assume  i in the carrier of S ; ::_thesis: C . i = D . i
then reconsider s = i as Element of S ;
 C . s = Class (R . s) by A3;
hence  C . i = D . i by A4; ::_thesis: verum
end;
hence  C = D by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Class MSUALG_4:def_6_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for b4 being V8() ManySortedSet of the carrier of S holds
( b4 = Class R iff for s being Element of S holds b4 . s = Class (R . s) );

begin

definition
let S be non empty non void ManySortedSign ;
let M1, M2 be ManySortedSet of the carrier' of S;
let F be ManySortedFunction of M1,M2;
let o be OperSymbol of S;
:: original: .
redefine funcF . o ->  Function of (M1 . o),(M2 . o);
coherence
 F . o is Function of (M1 . o),(M2 . o) by PBOOLE:def_15;
end;

registration
let I be non empty set ;
let p be FinSequence of I;
let X be ManySortedSet of I;
clusterp * X ->  dom p -defined for Function;
coherence
 for b1 being Function st b1 = X * p holds
b1 is dom p -defined
proof
 rng p c= I ;
then  rng p c= dom X by PARTFUN1:def_2;
then  dom (X * p) = dom p by RELAT_1:27;
then reconsider Xp = X * p as ManySortedSet of dom p by PARTFUN1:def_2, RELAT_1:def_18;
 Xp is ManySortedSet of dom p ;
hence  for b1 being Function st b1 = X * p holds
b1 is dom p -defined ; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let p be FinSequence of I;
let X be ManySortedSet of I;
clusterp * X ->  dom p -defined total for dom p -defined Function;
coherence
 for b1 being dom p -defined Function st b1 = X * p holds
b1 is total
proof
 rng p c= I ;
then  rng p c= dom X by PARTFUN1:def_2;
then  dom (X * p) = dom p by RELAT_1:27;
then reconsider Xp = X * p as ManySortedSet of dom p by PARTFUN1:def_2;
 Xp is ManySortedSet of dom p ;
hence  for b1 being dom p -defined Function st b1 = X * p holds
b1 is total ; ::_thesis: verum
end;
end;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
let x be Element of Args (o,A);
funcR # x ->  Element of product ((Class R) * (the_arity_of o)) means :Def7: :: MSUALG_4:def 7
 for n being Nat st n in dom (the_arity_of o) holds
it . n = Class ((R . ((the_arity_of o) /. n)),(x . n));
existence
 ex b1 being Element of product ((Class R) * (the_arity_of o)) st
for n being Nat st n in dom (the_arity_of o) holds
b1 . n = Class ((R . ((the_arity_of o) /. n)),(x . n))
proof
defpred S1[ set , set ] means  for n being Nat st n = $1 holds
$2 = Class ((R . ((the_arity_of o) /. n)),(x . n));
set ar = the_arity_of o;
set da = dom (the_arity_of o);
A1: for y being set st y in dom (the_arity_of o) holds
ex u being set st S1[y,u]
proof
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ex u being set st S1[y,u] )
assume  y in dom (the_arity_of o) ; ::_thesis: ex u being set st S1[y,u]
then reconsider n = y as Nat by ORDINAL1:def_12;
take  Class ((R . ((the_arity_of o) /. n)),(x . n)) ; ::_thesis: S1[y, Class ((R . ((the_arity_of o) /. n)),(x . n))]
thus  S1[y, Class ((R . ((the_arity_of o) /. n)),(x . n))] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = dom (the_arity_of o) & ( for x being set st x in dom (the_arity_of o) holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
A3: dom ((Class R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2;
 for y being set st y in dom ((Class R) * (the_arity_of o)) holds
f . y in ((Class R) * (the_arity_of o)) . y
proof
let y be set ; ::_thesis: ( y in dom ((Class R) * (the_arity_of o)) implies f . y in ((Class R) * (the_arity_of o)) . y )
assume A4: y in dom ((Class R) * (the_arity_of o)) ; ::_thesis: f . y in ((Class R) * (the_arity_of o)) . y
then reconsider n = y as Nat by ORDINAL1:def_12;
 (the_arity_of o) . y in rng (the_arity_of o) by A3, A4, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . y as Element of S ;
A5: y in dom ( the Sorts of A * (the_arity_of o)) by A3, A4, PARTFUN1:def_2;
then  ( the Sorts of A * (the_arity_of o)) . y = the Sorts of A . ((the_arity_of o) . y) by FUNCT_1:12;
then A6: x . y in the Sorts of A . s by A5, MSUALG_3:6;
 ( f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) & (the_arity_of o) /. n = (the_arity_of o) . n ) by A2, A3, A4, PARTFUN1:def_6;
then A7: f . y in Class (R . s) by A6, EQREL_1:def_3;
 ((Class R) * (the_arity_of o)) . y = (Class R) . ((the_arity_of o) . y) by A4, FUNCT_1:12;
hence  f . y in ((Class R) * (the_arity_of o)) . y by A7, Def6; ::_thesis: verum
end;
then reconsider f = f as Element of product ((Class R) * (the_arity_of o)) by A2, A3, CARD_3:9;
take  f ; ::_thesis: for n being Nat st n in dom (the_arity_of o) holds
f . n = Class ((R . ((the_arity_of o) /. n)),(x . n))
let n be Nat; ::_thesis: ( n in dom (the_arity_of o) implies f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) )
assume  n in dom (the_arity_of o) ; ::_thesis: f . n = Class ((R . ((the_arity_of o) /. n)),(x . n))
hence  f . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of product ((Class R) * (the_arity_of o)) st ( for n being Nat st n in dom (the_arity_of o) holds
b1 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) & ( for n being Nat st n in dom (the_arity_of o) holds
b2 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) holds
b1 = b2
proof
let F, G be Element of product ((Class R) * (the_arity_of o)); ::_thesis: ( ( for n being Nat st n in dom (the_arity_of o) holds
F . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) & ( for n being Nat st n in dom (the_arity_of o) holds
G . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) implies F = G )
assume that
A8: for n being Nat st n in dom (the_arity_of o) holds
F . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) and
A9: for n being Nat st n in dom (the_arity_of o) holds
G . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ; ::_thesis: F = G
A10: for y being set st y in dom (the_arity_of o) holds
F . y = G . y
proof
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies F . y = G . y )
assume A11: y in dom (the_arity_of o) ; ::_thesis: F . y = G . y
then reconsider n = y as Nat by ORDINAL1:def_12;
 F . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) by A8, A11;
hence  F . y = G . y by A9, A11; ::_thesis: verum
end;
A12: dom G = dom (the_arity_of o) by PARTFUN1:def_2;
 dom F = dom (the_arity_of o) by PARTFUN1:def_2;
hence  F = G by A12, A10, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines # MSUALG_4:def_7_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being Element of Args (o,A)
for b6 being Element of product ((Class R) * (the_arity_of o)) holds
( b6 = R # x iff for n being Nat st n in dom (the_arity_of o) holds
b6 . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) );

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotRes (R,o) ->  Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) means :Def8: :: MSUALG_4:def 8
 for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = Class (R,x);
existence
 ex b1 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st
for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (R,x)
proof
set rs = the_result_sort_of o;
set D = the Sorts of A . (the_result_sort_of o);
deffunc H1( Element of the Sorts of A . (the_result_sort_of o)) ->  Subset of ( the Sorts of A . (the_result_sort_of o)) = Class (R,$1);
consider f being Function such that
A1: ( dom f = the Sorts of A . (the_result_sort_of o) & ( for d being Element of the Sorts of A . (the_result_sort_of o) holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
A2: for x being set st x in the Sorts of A . (the_result_sort_of o) holds
f . x in (Class R) . (the_result_sort_of o)
proof
let x be set ; ::_thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x in (Class R) . (the_result_sort_of o) )
assume  x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: f . x in (Class R) . (the_result_sort_of o)
then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ;
 f . x1 = Class (R,x1) by A1;
then  f . x1 in Class (R . (the_result_sort_of o)) by EQREL_1:def_3;
hence  f . x in (Class R) . (the_result_sort_of o) by Def6; ::_thesis: verum
end;
 o in the carrier' of S ;
then  o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def_2;
then A3: ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2 ;
A4: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then  dom ((Class R) * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
then ((Class R) * the ResultSort of S) . o = (Class R) . ( the ResultSort of S . o) by A4, FUNCT_1:12
.= (Class R) . (the_result_sort_of o) by MSUALG_1:def_2 ;
then reconsider f = f as Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) by A1, A3, A2, FUNCT_2:3;
take  f ; ::_thesis: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x)
thus  for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) st ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b1 . x = Class (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b2 . x = Class (R,x) ) holds
b1 = b2
proof
set SA = the Sorts of A;
set RS = the ResultSort of S;
set rs = the_result_sort_of o;
let f, g be Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o); ::_thesis: ( ( for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = Class (R,x) ) implies f = g )
assume that
A5: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x) and
A6: for x being Element of the Sorts of A . (the_result_sort_of o) holds g . x = Class (R,x) ; ::_thesis: f = g
A7: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_A_._(the_result_sort_of_o)_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x = g . x )
assume  x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ;
 f . x1 = Class (R,x1) by A5;
hence  f . x = g . x by A6; ::_thesis: verum
end;
 o in the carrier' of S ;
then  o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def_2;
then ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2 ;
then  ( dom f = the Sorts of A . (the_result_sort_of o) & dom g = the Sorts of A . (the_result_sort_of o) ) by FUNCT_2:def_1;
hence  f = g by A7, FUNCT_1:2; ::_thesis: verum
end;
func QuotArgs (R,o) ->  Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) means :: MSUALG_4:def 9
 for x being Element of Args (o,A) holds it . x = R # x;
existence
 ex b1 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st
for x being Element of Args (o,A) holds b1 . x = R # x
proof
set ao = the_arity_of o;
set D = Args (o,A);
deffunc H1( Element of Args (o,A)) ->  Element of product ((Class R) * (the_arity_of o)) = R # $1;
consider f being Function such that
A8: ( dom f = Args (o,A) & ( for d being Element of Args (o,A) holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
A9: o in the carrier' of S ;
then  o in dom (( the Sorts of A #) * the Arity of S) by PARTFUN1:def_2;
then A10: (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . ( the Arity of S . o) by FUNCT_1:12
.= ( the Sorts of A #) . (the_arity_of o) by MSUALG_1:def_1 ;
A11: for x being set st x in ( the Sorts of A #) . (the_arity_of o) holds
f . x in ((Class R) #) . (the_arity_of o)
proof
let x be set ; ::_thesis: ( x in ( the Sorts of A #) . (the_arity_of o) implies f . x in ((Class R) #) . (the_arity_of o) )
assume  x in ( the Sorts of A #) . (the_arity_of o) ; ::_thesis: f . x in ((Class R) #) . (the_arity_of o)
then reconsider x1 = x as Element of Args (o,A) by A10, MSUALG_1:def_4;
 ( f . x1 = R # x1 & ((Class R) #) . (the_arity_of o) = product ((Class R) * (the_arity_of o)) ) by A8, FINSEQ_2:def_5;
hence  f . x in ((Class R) #) . (the_arity_of o) ; ::_thesis: verum
end;
 o in dom (((Class R) #) * the Arity of S) by A9, PARTFUN1:def_2;
then (((Class R) #) * the Arity of S) . o = ((Class R) #) . ( the Arity of S . o) by FUNCT_1:12
.= ((Class R) #) . (the_arity_of o) by MSUALG_1:def_1 ;
then reconsider f = f as Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) by A8, A10, A11, FUNCT_2:3, MSUALG_1:def_4;
take  f ; ::_thesis: for x being Element of Args (o,A) holds f . x = R # x
thus  for x being Element of Args (o,A) holds f . x = R # x by A8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) st ( for x being Element of Args (o,A) holds b1 . x = R # x ) & ( for x being Element of Args (o,A) holds b2 . x = R # x ) holds
b1 = b2
proof
set ao = the_arity_of o;
let f, g be Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o); ::_thesis: ( ( for x being Element of Args (o,A) holds f . x = R # x ) & ( for x being Element of Args (o,A) holds g . x = R # x ) implies f = g )
assume that
A12: for x being Element of Args (o,A) holds f . x = R # x and
A13: for x being Element of Args (o,A) holds g . x = R # x ; ::_thesis: f = g
 o in the carrier' of S ;
then  o in dom (( the Sorts of A #) * the Arity of S) by PARTFUN1:def_2;
then A14: (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . ( the Arity of S . o) by FUNCT_1:12
.= ( the Sorts of A #) . (the_arity_of o) by MSUALG_1:def_1 ;
A15: now__::_thesis:_for_x_being_set_st_x_in_(_the_Sorts_of_A_#)_._(the_arity_of_o)_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in ( the Sorts of A #) . (the_arity_of o) implies f . x = g . x )
assume  x in ( the Sorts of A #) . (the_arity_of o) ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of Args (o,A) by A14, MSUALG_1:def_4;
 f . x1 = R # x1 by A12;
hence  f . x = g . x by A13; ::_thesis: verum
end;
 ( dom f = ( the Sorts of A #) . (the_arity_of o) & dom g = ( the Sorts of A #) . (the_arity_of o) ) by A14, FUNCT_2:def_1;
hence  f = g by A15, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines QuotRes MSUALG_4:def_8_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b5 being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) holds
( b5 = QuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b5 . x = Class (R,x) );

:: deftheorem  defines QuotArgs MSUALG_4:def_9_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b5 being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) holds
( b5 = QuotArgs (R,o) iff for x being Element of Args (o,A) holds b5 . x = R # x );

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotRes R ->  ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S means :: MSUALG_4:def 10
 for o being OperSymbol of S holds it . o = QuotRes (R,o);
existence
 ex b1 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = QuotRes (R,o)
proof
defpred S1[ set , set ] means  for o being OperSymbol of S st o = $1 holds
$2 = QuotRes (R,o);
set O = the carrier' of S;
A1: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume  x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider x1 = x as OperSymbol of S ;
take  QuotRes (R,x1) ; ::_thesis: S1[x, QuotRes (R,x1)]
thus  S1[x, QuotRes (R,x1)] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
 for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume  x in dom f ; ::_thesis: f . x is Function
then reconsider x1 = x as OperSymbol of S ;
 f . x1 = QuotRes (R,x1) by A2;
hence  f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
 for i being set st i in the carrier' of S holds
f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((Class R) * the ResultSort of S) . i)
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((Class R) * the ResultSort of S) . i) )
assume  i in the carrier' of S ; ::_thesis: f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((Class R) * the ResultSort of S) . i)
then reconsider i1 = i as OperSymbol of S ;
 f . i1 = QuotRes (R,i1) by A2;
hence  f . i is Function of (( the Sorts of A * the ResultSort of S) . i),(((Class R) * the ResultSort of S) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S by PBOOLE:def_15;
take  f ; ::_thesis: for o being OperSymbol of S holds f . o = QuotRes (R,o)
thus  for o being OperSymbol of S holds f . o = QuotRes (R,o) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = QuotRes (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotRes (R,o) ) holds
b1 = b2
proof
let f, g be ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = QuotRes (R,o) ) & ( for o being OperSymbol of S holds g . o = QuotRes (R,o) ) implies f = g )
assume that
A3: for o being OperSymbol of S holds f . o = QuotRes (R,o) and
A4: for o being OperSymbol of S holds g . o = QuotRes (R,o) ; ::_thesis: f = g
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i )
assume  i in the carrier' of S ; ::_thesis: f . i = g . i
then reconsider i1 = i as OperSymbol of S ;
 f . i1 = QuotRes (R,i1) by A3;
hence  f . i = g . i by A4; ::_thesis: verum
end;
hence  f = g by PBOOLE:3; ::_thesis: verum
end;
func QuotArgs R ->  ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S means :: MSUALG_4:def 11
 for o being OperSymbol of S holds it . o = QuotArgs (R,o);
existence
 ex b1 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st
for o being OperSymbol of S holds b1 . o = QuotArgs (R,o)
proof
defpred S1[ set , set ] means  for o being OperSymbol of S st o = $1 holds
$2 = QuotArgs (R,o);
set O = the carrier' of S;
A5: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume  x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider x1 = x as OperSymbol of S ;
take  QuotArgs (R,x1) ; ::_thesis: S1[x, QuotArgs (R,x1)]
thus  S1[x, QuotArgs (R,x1)] ; ::_thesis: verum
end;
consider f being Function such that
A6: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A5);
reconsider f = f as ManySortedSet of the carrier' of S by A6, PARTFUN1:def_2, RELAT_1:def_18;
 for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume  x in dom f ; ::_thesis: f . x is Function
then reconsider x1 = x as OperSymbol of S ;
 f . x1 = QuotArgs (R,x1) by A6;
hence  f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
 for i being set st i in the carrier' of S holds
f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((Class R) #) * the Arity of S) . i)
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((Class R) #) * the Arity of S) . i) )
assume  i in the carrier' of S ; ::_thesis: f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((Class R) #) * the Arity of S) . i)
then reconsider i1 = i as OperSymbol of S ;
 f . i1 = QuotArgs (R,i1) by A6;
hence  f . i is Function of ((( the Sorts of A #) * the Arity of S) . i),((((Class R) #) * the Arity of S) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S by PBOOLE:def_15;
take  f ; ::_thesis: for o being OperSymbol of S holds f . o = QuotArgs (R,o)
thus  for o being OperSymbol of S holds f . o = QuotArgs (R,o) by A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S st ( for o being OperSymbol of S holds b1 . o = QuotArgs (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotArgs (R,o) ) holds
b1 = b2
proof
let f, g be ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = QuotArgs (R,o) ) & ( for o being OperSymbol of S holds g . o = QuotArgs (R,o) ) implies f = g )
assume that
A7: for o being OperSymbol of S holds f . o = QuotArgs (R,o) and
A8: for o being OperSymbol of S holds g . o = QuotArgs (R,o) ; ::_thesis: f = g
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i )
assume  i in the carrier' of S ; ::_thesis: f . i = g . i
then reconsider i1 = i as OperSymbol of S ;
 f . i1 = QuotArgs (R,i1) by A7;
hence  f . i = g . i by A8; ::_thesis: verum
end;
hence  f = g by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem  defines QuotRes MSUALG_4:def_10_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b4 being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S holds
( b4 = QuotRes R iff for o being OperSymbol of S holds b4 . o = QuotRes (R,o) );

:: deftheorem  defines QuotArgs MSUALG_4:def_11_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b4 being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S holds
( b4 = QuotArgs R iff for o being OperSymbol of S holds b4 . o = QuotArgs (R,o) );

theorem Th2: :: MSUALG_4:2
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let o be OperSymbol of S; ::_thesis: for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let A be non-empty MSAlgebra over S; ::_thesis: for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let R be MSCongruence of A; ::_thesis: for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a
let x be set ; ::_thesis: ( x in (((Class R) #) * the Arity of S) . o implies ex a being Element of Args (o,A) st x = R # a )
assume A1: x in (((Class R) #) * the Arity of S) . o ; ::_thesis: ex a being Element of Args (o,A) st x = R # a
set ar = the_arity_of o;
A2: the_arity_of o = the Arity of S . o by MSUALG_1:def_1;
then  (((Class R) #) * the Arity of S) . o = product ((Class R) * (the_arity_of o)) by MSAFREE:1;
then consider f being Function such that
A3: f = x and
A4: dom f = dom ((Class R) * (the_arity_of o)) and
A5: for y being set st y in dom ((Class R) * (the_arity_of o)) holds
f . y in ((Class R) * (the_arity_of o)) . y by A1, CARD_3:def_5;
defpred S1[ set , set ] means $2 in f . $1;
A6: dom ((Class R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2;
A7: for n being Nat st n in dom f holds
f . n in Class (R . ((the_arity_of o) /. n))
proof
let n be Nat; ::_thesis: ( n in dom f implies f . n in Class (R . ((the_arity_of o) /. n)) )
reconsider s = (the_arity_of o) /. n as Element of S ;
assume A8: n in dom f ; ::_thesis: f . n in Class (R . ((the_arity_of o) /. n))
then  (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, PARTFUN1:def_6;
then ((Class R) * (the_arity_of o)) . n = (Class R) . s by A4, A8, FUNCT_1:12
.= Class (R . s) by Def6 ;
hence  f . n in Class (R . ((the_arity_of o) /. n)) by A4, A5, A8; ::_thesis: verum
end;
A9: for a being set st a in dom f holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in dom f implies ex b being set st S1[a,b] )
reconsider s = (the_arity_of o) /. a as Element of S ;
assume A10: a in dom f ; ::_thesis: ex b being set st S1[a,b]
then reconsider n = a as Nat by A4, ORDINAL1:def_12;
 f . n in Class (R . s) by A7, A10;
then consider a1 being set  such that
A11: ( a1 in the Sorts of A . s & f . n = Class ((R . s),a1) ) by EQREL_1:def_3;
take  a1 ; ::_thesis: S1[a,a1]
thus  S1[a,a1] by A11, EQREL_1:20; ::_thesis: verum
end;
consider g being Function such that
A12: ( dom g = dom f & ( for a being set st a in dom f holds
S1[a,g . a] ) ) from CLASSES1:sch_1(A9);
 dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
then  rng (the_arity_of o) c= dom the Sorts of A ;
then A13: dom g = dom ( the Sorts of A * (the_arity_of o)) by A4, A6, A12, RELAT_1:27;
A14: for y being set st y in dom ( the Sorts of A * (the_arity_of o)) holds
g . y in ( the Sorts of A * (the_arity_of o)) . y
proof
let y be set ; ::_thesis: ( y in dom ( the Sorts of A * (the_arity_of o)) implies g . y in ( the Sorts of A * (the_arity_of o)) . y )
assume A15: y in dom ( the Sorts of A * (the_arity_of o)) ; ::_thesis: g . y in ( the Sorts of A * (the_arity_of o)) . y
then A16: ( g . y in f . y & f . y in ((Class R) * (the_arity_of o)) . y ) by A4, A5, A12, A13;
reconsider n = y as Nat by A15, ORDINAL1:def_12;
reconsider s = (the_arity_of o) /. n as Element of S ;
A17: (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, A12, A13, A15, PARTFUN1:def_6;
then ((Class R) * (the_arity_of o)) . y = (Class R) . s by A4, A12, A13, A15, FUNCT_1:12
.= Class (R . s) by Def6 ;
then  g . n in the Sorts of A . s by A16;
hence  g . y in ( the Sorts of A * (the_arity_of o)) . y by A15, A17, FUNCT_1:12; ::_thesis: verum
end;
Args (o,A) = (( the Sorts of A #) * the Arity of S) . o by MSUALG_1:def_4
.= product ( the Sorts of A * (the_arity_of o)) by A2, MSAFREE:1 ;
then reconsider g = g as Element of Args (o,A) by A13, A14, CARD_3:9;
A18: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_arity_of_o)_holds_
f_._x_=_(R_#_g)_._x
let x be set ; ::_thesis: ( x in dom (the_arity_of o) implies f . x = (R # g) . x )
assume A19: x in dom (the_arity_of o) ; ::_thesis: f . x = (R # g) . x
then reconsider n = x as Nat by ORDINAL1:def_12;
reconsider s = (the_arity_of o) /. n as Element of S ;
 f . n in Class (R . s) by A4, A6, A7, A19;
then consider a1 being set  such that
A20: a1 in the Sorts of A . s and
A21: f . n = Class ((R . s),a1) by EQREL_1:def_3;
 g . n in f . n by A4, A6, A12, A19;
then  Class ((R . s),(g . n)) = Class ((R . s),a1) by A20, A21, EQREL_1:23;
hence  f . x = (R # g) . x by A19, A21, Def7; ::_thesis: verum
end;
take  g ; ::_thesis: x = R # g
 dom (R # g) = dom ((Class R) * (the_arity_of o)) by CARD_3:9;
hence  x = R # g by A3, A4, A6, A18, FUNCT_1:2; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotCharact (R,o) ->  Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) means :Def12: :: MSUALG_4:def 12
 for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
it . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a;
existence
 ex b1 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st
for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a
proof
defpred S1[ set , set ] means  for a being Element of Args (o,A) st $1 = R # a holds
$2 = ((QuotRes (R,o)) * (Den (o,A))) . a;
set Ca = (((Class R) #) * the Arity of S) . o;
set Cr = ((Class R) * the ResultSort of S) . o;
A1: for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex y being set st
( y in ((Class R) * the ResultSort of S) . o & S1[x,y] )
proof
set ro = the_result_sort_of o;
set ar = the_arity_of o;
let x be set ; ::_thesis: ( x in (((Class R) #) * the Arity of S) . o implies ex y being set st
( y in ((Class R) * the ResultSort of S) . o & S1[x,y] ) )
assume  x in (((Class R) #) * the Arity of S) . o ; ::_thesis: ex y being set st
( y in ((Class R) * the ResultSort of S) . o & S1[x,y] )
then consider a being Element of Args (o,A) such that
A2: x = R # a by Th2;
take y = ((QuotRes (R,o)) * (Den (o,A))) . a; ::_thesis: ( y in ((Class R) * the ResultSort of S) . o & S1[x,y] )
A3: o in the carrier' of S ;
then  o in dom ((Class R) * the ResultSort of S) by PARTFUN1:def_2;
then A4: ((Class R) * the ResultSort of S) . o = (Class R) . ( the ResultSort of S . o) by FUNCT_1:12
.= (Class R) . (the_result_sort_of o) by MSUALG_1:def_2 ;
 o in dom ( the Sorts of A * the ResultSort of S) by A3, PARTFUN1:def_2;
then A5: ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2 ;
then A6: ( dom (QuotRes (R,o)) = the Sorts of A . (the_result_sort_of o) & Result (o,A) = the Sorts of A . (the_result_sort_of o) ) by FUNCT_2:def_1, MSUALG_1:def_5;
 rng (Den (o,A)) c= Result (o,A) ;
then A7: ( dom (Den (o,A)) = Args (o,A) & dom ((QuotRes (R,o)) * (Den (o,A))) = dom (Den (o,A)) ) by A6, FUNCT_2:def_1, RELAT_1:27;
 (QuotRes (R,o)) . ((Den (o,A)) . a) in rng (QuotRes (R,o)) by A6, FUNCT_1:def_3;
then  (QuotRes (R,o)) . ((Den (o,A)) . a) in (Class R) . (the_result_sort_of o) by A4;
hence  y in ((Class R) * the ResultSort of S) . o by A4, A7, FUNCT_1:12; ::_thesis: S1[x,y]
let b be Element of Args (o,A); ::_thesis: ( x = R # b implies y = ((QuotRes (R,o)) * (Den (o,A))) . b )
reconsider da = (Den (o,A)) . a, db = (Den (o,A)) . b as Element of the Sorts of A . (the_result_sort_of o) by A5, MSUALG_1:def_5;
A8: ((QuotRes (R,o)) * (Den (o,A))) . b = (QuotRes (R,o)) . db by A7, FUNCT_1:12
.= Class (R,db) by Def8
.= Class ((R . (the_result_sort_of o)),db) ;
assume A9: x = R # b ; ::_thesis: y = ((QuotRes (R,o)) * (Den (o,A))) . b
 for n being Nat st n in dom a holds
[(a . n),(b . n)] in R . ((the_arity_of o) /. n)
proof
let n be Nat; ::_thesis: ( n in dom a implies [(a . n),(b . n)] in R . ((the_arity_of o) /. n) )
A10: dom a = dom (the_arity_of o) by MSUALG_3:6;
assume A11: n in dom a ; ::_thesis: [(a . n),(b . n)] in R . ((the_arity_of o) /. n)
then A12: ( (R # a) . n = Class ((R . ((the_arity_of o) /. n)),(a . n)) & (R # b) . n = Class ((R . ((the_arity_of o) /. n)),(b . n)) ) by A10, Def7;
 dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
then  rng (the_arity_of o) c= dom the Sorts of A ;
then A13: dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
then A14: a . n in ( the Sorts of A * (the_arity_of o)) . n by A11, A10, MSUALG_3:6;
( the Sorts of A * (the_arity_of o)) . n = the Sorts of A . ((the_arity_of o) . n) by A13, A11, A10, FUNCT_1:12
.= the Sorts of A . ((the_arity_of o) /. n) by A11, A10, PARTFUN1:def_6 ;
hence  [(a . n),(b . n)] in R . ((the_arity_of o) /. n) by A2, A9, A14, A12, EQREL_1:35; ::_thesis: verum
end;
then A15: [da,db] in R . (the_result_sort_of o) by Def4;
y = (QuotRes (R,o)) . ((Den (o,A)) . a) by A7, FUNCT_1:12
.= Class (R,da) by Def8
.= Class ((R . (the_result_sort_of o)),da) ;
hence  y = ((QuotRes (R,o)) * (Den (o,A))) . b by A8, A15, EQREL_1:35; ::_thesis: verum
end;
consider f being Function such that
A16: ( dom f = (((Class R) #) * the Arity of S) . o & rng f c= ((Class R) * the ResultSort of S) . o & ( for x being set st x in (((Class R) #) * the Arity of S) . o holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A1);
reconsider f = f as Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) by A16, FUNCT_2:2;
take  f ; ::_thesis: for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
f . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a
thus  for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
f . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a by A16; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) st ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b1 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b2 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) holds
b1 = b2
proof
set ao = the_arity_of o;
let F, G be Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o); ::_thesis: ( ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
F . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) & ( for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
G . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) implies F = G )
assume that
A17: for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
F . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a and
A18: for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
G . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ; ::_thesis: F = G
A19: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then  dom (((Class R) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2;
then A20: (((Class R) #) * the Arity of S) . o = ((Class R) #) . ( the Arity of S . o) by A19, FUNCT_1:12
.= ((Class R) #) . (the_arity_of o) by MSUALG_1:def_1 ;
A21: now__::_thesis:_for_x_being_set_st_x_in_((Class_R)_#)_._(the_arity_of_o)_holds_
F_._x_=_G_._x
let x be set ; ::_thesis: ( x in ((Class R) #) . (the_arity_of o) implies F . x = G . x )
assume A22: x in ((Class R) #) . (the_arity_of o) ; ::_thesis: F . x = G . x
then consider a being Element of Args (o,A) such that
A23: x = R # a by A20, Th2;
 F . x = ((QuotRes (R,o)) * (Den (o,A))) . a by A17, A20, A22, A23;
hence  F . x = G . x by A18, A20, A22, A23; ::_thesis: verum
end;
 ( dom F = ((Class R) #) . (the_arity_of o) & dom G = ((Class R) #) . (the_arity_of o) ) by A20, FUNCT_2:def_1;
hence  F = G by A21, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines QuotCharact MSUALG_4:def_12_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b5 being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) holds
( b5 = QuotCharact (R,o) iff for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds
b5 . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a );

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let R be MSCongruence of A;
func QuotCharact R ->  ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S means :Def13: :: MSUALG_4:def 13
 for o being OperSymbol of S holds it . o = QuotCharact (R,o);
existence
 ex b1 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = QuotCharact (R,o)
proof
defpred S1[ set , set ] means  for o being OperSymbol of S st o = $1 holds
$2 = QuotCharact (R,o);
set O = the carrier' of S;
A1: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume  x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider x1 = x as OperSymbol of S ;
take  QuotCharact (R,x1) ; ::_thesis: S1[x, QuotCharact (R,x1)]
thus  S1[x, QuotCharact (R,x1)] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
 for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume  x in dom f ; ::_thesis: f . x is Function
then reconsider x1 = x as OperSymbol of S ;
 f . x1 = QuotCharact (R,x1) by A2;
hence  f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
 for i being set st i in the carrier' of S holds
f . i is Function of ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i)
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i is Function of ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i) )
assume  i in the carrier' of S ; ::_thesis: f . i is Function of ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i)
then reconsider i1 = i as OperSymbol of S ;
 f . i1 = QuotCharact (R,i1) by A2;
hence  f . i is Function of ((((Class R) #) * the Arity of S) . i),(((Class R) * the ResultSort of S) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S by PBOOLE:def_15;
take  f ; ::_thesis: for o being OperSymbol of S holds f . o = QuotCharact (R,o)
thus  for o being OperSymbol of S holds f . o = QuotCharact (R,o) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = QuotCharact (R,o) ) & ( for o being OperSymbol of S holds b2 . o = QuotCharact (R,o) ) holds
b1 = b2
proof
let f, g be ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds f . o = QuotCharact (R,o) ) & ( for o being OperSymbol of S holds g . o = QuotCharact (R,o) ) implies f = g )
assume that
A3: for o being OperSymbol of S holds f . o = QuotCharact (R,o) and
A4: for o being OperSymbol of S holds g . o = QuotCharact (R,o) ; ::_thesis: f = g
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_
f_._i_=_g_._i
let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i )
assume  i in the carrier' of S ; ::_thesis: f . i = g . i
then reconsider i1 = i as OperSymbol of S ;
 f . i1 = QuotCharact (R,i1) by A3;
hence  f . i = g . i by A4; ::_thesis: verum
end;
hence  f = g by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines QuotCharact MSUALG_4:def_13_:_
 for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b4 being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S holds
( b4 = QuotCharact R iff for o being OperSymbol of S holds b4 . o = QuotCharact (R,o) );

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func QuotMSAlg (U1,R) ->  MSAlgebra over S equals :: MSUALG_4:def 14
 MSAlgebra(# (Class R),(QuotCharact R) #);
coherence
 MSAlgebra(# (Class R),(QuotCharact R) #) is MSAlgebra over S ;
end;

:: deftheorem  defines QuotMSAlg MSUALG_4:def_14_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1 holds QuotMSAlg (U1,R) = MSAlgebra(# (Class R),(QuotCharact R) #);

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
cluster QuotMSAlg (U1,R) ->  strict non-empty ;
coherence
 ( QuotMSAlg (U1,R) is strict & QuotMSAlg (U1,R) is non-empty ) by MSUALG_1:def_3;
end;

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
let s be SortSymbol of S;
func MSNat_Hom (U1,R,s) ->  Function of ( the Sorts of U1 . s),((Class R) . s) means :Def15: :: MSUALG_4:def 15
 for x being set st x in the Sorts of U1 . s holds
it . x = Class ((R . s),x);
existence
 ex b1 being Function of ( the Sorts of U1 . s),((Class R) . s) st
for x being set st x in the Sorts of U1 . s holds
b1 . x = Class ((R . s),x)
proof
deffunc H1( set ) ->  Element of K10(( the Sorts of U1 . s)) = Class ((R . s),$1);
consider f being Function such that
A1: ( dom f = the Sorts of U1 . s & ( for x being set st x in the Sorts of U1 . s holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
 for x being set st x in the Sorts of U1 . s holds
f . x in (Class R) . s
proof
let x be set ; ::_thesis: ( x in the Sorts of U1 . s implies f . x in (Class R) . s )
assume A2: x in the Sorts of U1 . s ; ::_thesis: f . x in (Class R) . s
then  Class ((R . s),x) in Class (R . s) by EQREL_1:def_3;
then  f . x in Class (R . s) by A1, A2;
hence  f . x in (Class R) . s by Def6; ::_thesis: verum
end;
then reconsider f = f as Function of ( the Sorts of U1 . s),((Class R) . s) by A1, FUNCT_2:3;
take  f ; ::_thesis: for x being set st x in the Sorts of U1 . s holds
f . x = Class ((R . s),x)
thus  for x being set st x in the Sorts of U1 . s holds
f . x = Class ((R . s),x) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of ( the Sorts of U1 . s),((Class R) . s) st ( for x being set st x in the Sorts of U1 . s holds
b1 . x = Class ((R . s),x) ) & ( for x being set st x in the Sorts of U1 . s holds
b2 . x = Class ((R . s),x) ) holds
b1 = b2
proof
let f, g be Function of ( the Sorts of U1 . s),((Class R) . s); ::_thesis: ( ( for x being set st x in the Sorts of U1 . s holds
f . x = Class ((R . s),x) ) & ( for x being set st x in the Sorts of U1 . s holds
g . x = Class ((R . s),x) ) implies f = g )
assume that
A3: for x being set st x in the Sorts of U1 . s holds
f . x = Class ((R . s),x) and
A4: for x being set st x in the Sorts of U1 . s holds
g . x = Class ((R . s),x) ; ::_thesis: f = g
A5: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_U1_._s_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the Sorts of U1 . s implies f . x = g . x )
assume A6: x in the Sorts of U1 . s ; ::_thesis: f . x = g . x
then  f . x = Class ((R . s),x) by A3;
hence  f . x = g . x by A4, A6; ::_thesis: verum
end;
 ( dom f = the Sorts of U1 . s & dom g = the Sorts of U1 . s ) by FUNCT_2:def_1;
hence  f = g by A5, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines MSNat_Hom MSUALG_4:def_15_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for s being SortSymbol of S
for b5 being Function of ( the Sorts of U1 . s),((Class R) . s) holds
( b5 = MSNat_Hom (U1,R,s) iff for x being set st x in the Sorts of U1 . s holds
b5 . x = Class ((R . s),x) );

definition
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let R be MSCongruence of U1;
func MSNat_Hom (U1,R) ->  ManySortedFunction of U1,(QuotMSAlg (U1,R)) means :Def16: :: MSUALG_4:def 16
 for s being SortSymbol of S holds it . s = MSNat_Hom (U1,R,s);
existence
 ex b1 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st
for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s)
proof
deffunc H1( Element of S) ->  Function of ( the Sorts of U1 . $1),((Class R) . $1) = MSNat_Hom (U1,R,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
 for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume  x in dom f ; ::_thesis: f . x is Function
then reconsider y = x as Element of S ;
 f . y = MSNat_Hom (U1,R,y) by A1;
hence  f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6;
 for i being set st i in the carrier of S holds
f . i is Function of ( the Sorts of U1 . i),((Class R) . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of U1 . i),((Class R) . i) )
assume  i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of U1 . i),((Class R) . i)
then reconsider s = i as Element of S ;
 f . s = MSNat_Hom (U1,R,s) by A1;
hence  f . i is Function of ( the Sorts of U1 . i),((Class R) . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Sorts of U1, Class R by PBOOLE:def_15;
reconsider f = f as ManySortedFunction of U1,(QuotMSAlg (U1,R)) ;
take  f ; ::_thesis: for s being SortSymbol of S holds f . s = MSNat_Hom (U1,R,s)
thus  for s being SortSymbol of S holds f . s = MSNat_Hom (U1,R,s) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st ( for s being SortSymbol of S holds b1 . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds b2 . s = MSNat_Hom (U1,R,s) ) holds
b1 = b2
proof
let F, G be ManySortedFunction of U1,(QuotMSAlg (U1,R)); ::_thesis: ( ( for s being SortSymbol of S holds F . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds G . s = MSNat_Hom (U1,R,s) ) implies F = G )
assume that
A2: for s being SortSymbol of S holds F . s = MSNat_Hom (U1,R,s) and
A3: for s being SortSymbol of S holds G . s = MSNat_Hom (U1,R,s) ; ::_thesis: F = G
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
F_._i_=_G_._i
let i be set ; ::_thesis: ( i in the carrier of S implies F . i = G . i )
assume  i in the carrier of S ; ::_thesis: F . i = G . i
then reconsider s = i as SortSymbol of S ;
 F . s = MSNat_Hom (U1,R,s) by A2;
hence  F . i = G . i by A3; ::_thesis: verum
end;
hence  F = G by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines MSNat_Hom MSUALG_4:def_16_:_
 for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for b4 being ManySortedFunction of U1,(QuotMSAlg (U1,R)) holds
( b4 = MSNat_Hom (U1,R) iff for s being SortSymbol of S holds b4 . s = MSNat_Hom (U1,R,s) );

theorem :: MSUALG_4:3
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R)
let U1 be non-empty MSAlgebra over S; ::_thesis: for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R)
let R be MSCongruence of U1; ::_thesis: MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R)
set F = MSNat_Hom (U1,R);
set QA = QuotMSAlg (U1,R);
set S1 = the Sorts of U1;
 for o being OperSymbol of S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x)
proof
let o be OperSymbol of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) )
assume  Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x)
let x be Element of Args (o,U1); ::_thesis: ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x)
set ro = the_result_sort_of o;
set ar = the_arity_of o;
 the Arity of S . o = the_arity_of o by MSUALG_1:def_1;
then A1: (((Class R) #) * the Arity of S) . o = product ((Class R) * (the_arity_of o)) by MSAFREE:1;
A2: dom x = dom (the_arity_of o) by MSUALG_3:6;
A3: for a being set st a in dom (the_arity_of o) holds
((MSNat_Hom (U1,R)) # x) . a = (R # x) . a
proof
let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies ((MSNat_Hom (U1,R)) # x) . a = (R # x) . a )
assume A4: a in dom (the_arity_of o) ; ::_thesis: ((MSNat_Hom (U1,R)) # x) . a = (R # x) . a
then reconsider n = a as Nat by ORDINAL1:def_12;
set Fo = MSNat_Hom (U1,R,((the_arity_of o) /. n));
set s = (the_arity_of o) /. n;
A5: n in dom ( the Sorts of U1 * (the_arity_of o)) by A4, PARTFUN1:def_2;
then ( the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) . n) by FUNCT_1:12
.= the Sorts of U1 . ((the_arity_of o) /. n) by A4, PARTFUN1:def_6 ;
then reconsider xn = x . n as Element of the Sorts of U1 . ((the_arity_of o) /. n) by A5, MSUALG_3:6;
thus ((MSNat_Hom (U1,R)) # x) . a = ((MSNat_Hom (U1,R)) . ((the_arity_of o) /. n)) . (x . n) by A2, A4, MSUALG_3:def_6
.= (MSNat_Hom (U1,R,((the_arity_of o) /. n))) . xn by Def16
.= Class ((R . ((the_arity_of o) /. n)),(x . n)) by Def15
.= (R # x) . a by A4, Def7 ; ::_thesis: verum
end;
 dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then  rng the ResultSort of S c= dom the Sorts of U1 ;
then  ( dom the ResultSort of S = the carrier' of S & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by FUNCT_2:def_1, RELAT_1:27;
then A6: ( the Sorts of U1 * the ResultSort of S) . o = the Sorts of U1 . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then reconsider dx = (Den (o,U1)) . x as Element of the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_5;
 ( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) by A6, MSUALG_1:def_5;
then  rng (Den (o,U1)) c= dom (QuotRes (R,o)) by A6, FUNCT_2:def_1;
then A7: ( dom (Den (o,U1)) = Args (o,U1) & dom ((QuotRes (R,o)) * (Den (o,U1))) = dom (Den (o,U1)) ) by FUNCT_2:def_1, RELAT_1:27;
 dom (Class R) = the carrier of S by PARTFUN1:def_2;
then  ( dom (R # x) = dom ((Class R) * (the_arity_of o)) & rng (the_arity_of o) c= dom (Class R) ) by CARD_3:9;
then  ( dom ((MSNat_Hom (U1,R)) # x) = dom (the_arity_of o) & dom (R # x) = dom (the_arity_of o) ) by MSUALG_3:6, RELAT_1:27;
then A8: (MSNat_Hom (U1,R)) # x = R # x by A3, FUNCT_1:2;
Den (o,(QuotMSAlg (U1,R))) = (QuotCharact R) . o by MSUALG_1:def_6
.= QuotCharact (R,o) by Def13 ;
then (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) = ((QuotRes (R,o)) * (Den (o,U1))) . x by A1, A8, Def12
.= (QuotRes (R,o)) . dx by A7, FUNCT_1:12
.= Class (R,dx) by Def8
.= (MSNat_Hom (U1,R,(the_result_sort_of o))) . dx by Def15
.= ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) by Def16 ;
hence  ((MSNat_Hom (U1,R)) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(QuotMSAlg (U1,R)))) . ((MSNat_Hom (U1,R)) # x) ; ::_thesis: verum
end;
hence  MSNat_Hom (U1,R) is_homomorphism U1, QuotMSAlg (U1,R) by MSUALG_3:def_7; :: according to MSUALG_3:def_8 ::_thesis: MSNat_Hom (U1,R) is "onto"
 for i being set st i in the carrier of S holds
rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i )
assume  i in the carrier of S ; ::_thesis: rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i
then reconsider s = i as Element of S ;
reconsider f = (MSNat_Hom (U1,R)) . i as Function of ( the Sorts of U1 . s),( the Sorts of (QuotMSAlg (U1,R)) . s) by PBOOLE:def_15;
A9: dom f = the Sorts of U1 . s by FUNCT_2:def_1;
A10: the Sorts of (QuotMSAlg (U1,R)) . s = Class (R . s) by Def6;
 for x being set st x in the Sorts of (QuotMSAlg (U1,R)) . i holds
x in rng f
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotMSAlg (U1,R)) . i implies x in rng f )
A11: f = MSNat_Hom (U1,R,s) by Def16;
assume  x in the Sorts of (QuotMSAlg (U1,R)) . i ; ::_thesis: x in rng f
then consider a1 being set  such that
A12: a1 in the Sorts of U1 . s and
A13: x = Class ((R . s),a1) by A10, EQREL_1:def_3;
 f . a1 in rng f by A9, A12, FUNCT_1:def_3;
hence  x in rng f by A12, A13, A11, Def15; ::_thesis: verum
end;
then  the Sorts of (QuotMSAlg (U1,R)) . i c= rng f by TARSKI:def_3;
hence  rng ((MSNat_Hom (U1,R)) . i) = the Sorts of (QuotMSAlg (U1,R)) . i by XBOOLE_0:def_10; ::_thesis: verum
end;
hence  MSNat_Hom (U1,R) is "onto" by MSUALG_3:def_3; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
let s be SortSymbol of S;
func MSCng (F,s) ->  Equivalence_Relation of ( the Sorts of U1 . s) means :Def17: :: MSUALG_4:def 17
 for x, y being Element of the Sorts of U1 . s holds
( [x,y] in it iff (F . s) . x = (F . s) . y );
existence
 ex b1 being Equivalence_Relation of ( the Sorts of U1 . s) st
for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b1 iff (F . s) . x = (F . s) . y )
proof
defpred S1[ set , set ] means (F . s) . $1 = (F . s) . $2;
set S1 = the Sorts of U1 . s;
A1: for x, y being set st S1[x,y] holds
S1[y,x] ;
A2: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] ;
A3: for x being set st x in the Sorts of U1 . s holds
S1[x,x] ;
consider R being Equivalence_Relation of ( the Sorts of U1 . s) such that
A4: for x, y being set holds
( [x,y] in R iff ( x in the Sorts of U1 . s & y in the Sorts of U1 . s & S1[x,y] ) ) from EQREL_1:sch_1(A3, A1, A2);
take  R ; ::_thesis: for x, y being Element of the Sorts of U1 . s holds
( [x,y] in R iff (F . s) . x = (F . s) . y )
let x, y be Element of the Sorts of U1 . s; ::_thesis: ( [x,y] in R iff (F . s) . x = (F . s) . y )
thus  ( [x,y] in R iff (F . s) . x = (F . s) . y ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Equivalence_Relation of ( the Sorts of U1 . s) st ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b1 iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b2 iff (F . s) . x = (F . s) . y ) ) holds
b1 = b2
proof
let R, S be Equivalence_Relation of ( the Sorts of U1 . s); ::_thesis: ( ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in R iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in S iff (F . s) . x = (F . s) . y ) ) implies R = S )
assume that
A5: for x, y being Element of the Sorts of U1 . s holds
( [x,y] in R iff (F . s) . x = (F . s) . y ) and
A6: for x, y being Element of the Sorts of U1 . s holds
( [x,y] in S iff (F . s) . x = (F . s) . y ) ; ::_thesis: R = S
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_R_implies_[x,y]_in_S_)_&_(_[x,y]_in_S_implies_[x,y]_in_R_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in R implies [x,y] in S ) & ( [x,y] in S implies [x,y] in R ) )
thus  ( [x,y] in R implies [x,y] in S ) ::_thesis: ( [x,y] in S implies [x,y] in R )
proof
assume A7: [x,y] in R ; ::_thesis: [x,y] in S
then reconsider a = x, b = y as Element of the Sorts of U1 . s by ZFMISC_1:87;
 (F . s) . a = (F . s) . b by A5, A7;
hence  [x,y] in S by A6; ::_thesis: verum
end;
assume A8: [x,y] in S ; ::_thesis: [x,y] in R
then reconsider a = x, b = y as Element of the Sorts of U1 . s by ZFMISC_1:87;
 (F . s) . a = (F . s) . b by A6, A8;
hence  [x,y] in R by A5; ::_thesis: verum
end;
hence  R = S by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines MSCng MSUALG_4:def_17_:_
 for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S
for b6 being Equivalence_Relation of ( the Sorts of U1 . s) holds
( b6 = MSCng (F,s) iff for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b6 iff (F . s) . x = (F . s) . y ) );

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2 ;
func MSCng F ->  MSCongruence of U1 means :Def18: :: MSUALG_4:def 18
 for s being SortSymbol of S holds it . s = MSCng (F,s);
existence
 ex b1 being MSCongruence of U1 st
for s being SortSymbol of S holds b1 . s = MSCng (F,s)
proof
deffunc H1( Element of S) ->  Equivalence_Relation of ( the Sorts of U1 . $1) = MSCng (F,$1);
consider f being Function such that
A2: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
 for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) )
assume  i in the carrier of S ; ::_thesis: f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i)
then reconsider s = i as Element of S ;
 f . i = MSCng (F,s) by A2;
hence  f . i is Relation of ( the Sorts of U1 . i),( the Sorts of U1 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedRelation of the Sorts of U1 by Def1;
reconsider f = f as ManySortedRelation of U1 ;
 for i being set
for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
proof
let i be set ; ::_thesis: for R being Relation of ( the Sorts of U1 . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of U1 . i)
let R be Relation of ( the Sorts of U1 . i); ::_thesis: ( i in the carrier of S & f . i = R implies R is Equivalence_Relation of ( the Sorts of U1 . i) )
assume that
A3: i in the carrier of S and
A4: f . i = R ; ::_thesis: R is Equivalence_Relation of ( the Sorts of U1 . i)
reconsider s = i as Element of S by A3;
 R = MSCng (F,s) by A2, A4;
hence  R is Equivalence_Relation of ( the Sorts of U1 . i) ; ::_thesis: verum
end;
then  f is MSEquivalence_Relation-like by Def2;
then reconsider f = f as MSEquivalence-like ManySortedRelation of U1 by Def3;
 for o being OperSymbol of S
for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
proof
let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,U1) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) holds
[((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
let x, y be Element of Args (o,U1); ::_thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ) implies [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) )
set ao = the_arity_of o;
set ro = the_result_sort_of o;
set S1 = the Sorts of U1;
A5: dom x = dom (the_arity_of o) by MSUALG_3:6;
A6: dom y = dom (the_arity_of o) by MSUALG_3:6;
assume A7: for n being Nat st n in dom x holds
[(x . n),(y . n)] in f . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o)
A8: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_
(F_#_x)_._n_=_(F_#_y)_._n
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies (F # x) . n = (F # y) . n )
assume A9: n in dom (the_arity_of o) ; ::_thesis: (F # x) . n = (F # y) . n
then reconsider m = n as Nat by ORDINAL1:def_12;
A10: ( (F # x) . m = (F . ((the_arity_of o) /. m)) . (x . m) & (F # y) . m = (F . ((the_arity_of o) /. m)) . (y . m) ) by A5, A6, A9, MSUALG_3:def_6;
 (the_arity_of o) . m in rng (the_arity_of o) by A9, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . m as SortSymbol of S ;
A11: n in dom ( the Sorts of U1 * (the_arity_of o)) by A9, PARTFUN1:def_2;
then  ( x . m in ( the Sorts of U1 * (the_arity_of o)) . n & y . m in ( the Sorts of U1 * (the_arity_of o)) . n ) by MSUALG_3:6;
then reconsider x1 = x . m, y1 = y . m as Element of the Sorts of U1 . s by A11, FUNCT_1:12;
A12: [x1,y1] in f . ((the_arity_of o) /. m) by A7, A5, A9;
A13: (the_arity_of o) /. m = (the_arity_of o) . m by A9, PARTFUN1:def_6;
then  f . ((the_arity_of o) /. m) = MSCng (F,s) by A2;
hence  (F # x) . n = (F # y) . n by A10, A13, A12, Def17; ::_thesis: verum
end;
 ( dom (F # x) = dom (the_arity_of o) & dom (F # y) = dom (the_arity_of o) ) by MSUALG_3:6;
then A14: F # x = F # y by A8, FUNCT_1:2;
reconsider ro = the_result_sort_of o as SortSymbol of S ;
A15: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then A16: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . o) by A15, A16, FUNCT_1:12
.= the Sorts of U1 . ro by MSUALG_1:def_2 ;
then reconsider Dx = (Den (o,U1)) . x, Dy = (Den (o,U1)) . y as Element of the Sorts of U1 . ro ;
A17: (F . ro) . Dy = (Den (o,U2)) . (F # y) by A1, MSUALG_3:def_7;
 ( f . ro = MSCng (F,ro) & (F . ro) . Dx = (Den (o,U2)) . (F # x) ) by A1, A2, MSUALG_3:def_7;
hence  [((Den (o,U1)) . x),((Den (o,U1)) . y)] in f . (the_result_sort_of o) by A14, A17, Def17; ::_thesis: verum
end;
then reconsider f = f as MSCongruence of U1 by Def4;
take  f ; ::_thesis: for s being SortSymbol of S holds f . s = MSCng (F,s)
thus  for s being SortSymbol of S holds f . s = MSCng (F,s) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being MSCongruence of U1 st ( for s being SortSymbol of S holds b1 . s = MSCng (F,s) ) & ( for s being SortSymbol of S holds b2 . s = MSCng (F,s) ) holds
b1 = b2
proof
let C1, C2 be MSCongruence of U1; ::_thesis: ( ( for s being SortSymbol of S holds C1 . s = MSCng (F,s) ) & ( for s being SortSymbol of S holds C2 . s = MSCng (F,s) ) implies C1 = C2 )
assume that
A18: for s being SortSymbol of S holds C1 . s = MSCng (F,s) and
A19: for s being SortSymbol of S holds C2 . s = MSCng (F,s) ; ::_thesis: C1 = C2
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
C1_._i_=_C2_._i
let i be set ; ::_thesis: ( i in the carrier of S implies C1 . i = C2 . i )
assume  i in the carrier of S ; ::_thesis: C1 . i = C2 . i
then reconsider s = i as Element of S ;
 C1 . s = MSCng (F,s) by A18;
hence  C1 . i = C2 . i by A19; ::_thesis: verum
end;
hence  C1 = C2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def18 defines MSCng MSUALG_4:def_18_:_
 for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
for b5 being MSCongruence of U1 holds
( b5 = MSCng F iff for s being SortSymbol of S holds b5 . s = MSCng (F,s) );

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
let s be SortSymbol of S;
assume A1: F is_homomorphism U1,U2 ;
func MSHomQuot (F,s) ->  Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) means :Def19: :: MSUALG_4:def 19
 for x being Element of the Sorts of U1 . s holds it . (Class ((MSCng (F,s)),x)) = (F . s) . x;
existence
 ex b1 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st
for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x
proof
set qa = QuotMSAlg (U1,(MSCng F));
set cqa = the Sorts of (QuotMSAlg (U1,(MSCng F)));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
defpred S1[ set , set ] means  for a being Element of the Sorts of U1 . s st $1 = Class ((MSCng (F,s)),a) holds
$2 = (F . s) . a;
A2: the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) by Def6
.= Class (MSCng (F,s)) by A1, Def18 ;
A3: for x being set st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds
ex y being set st
( y in the Sorts of U2 . s & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s implies ex y being set st
( y in the Sorts of U2 . s & S1[x,y] ) )
assume A4: x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s ; ::_thesis: ex y being set st
( y in the Sorts of U2 . s & S1[x,y] )
then reconsider x1 = x as Subset of ( the Sorts of U1 . s) by A2;
consider a being set  such that
A5: a in the Sorts of U1 . s and
A6: x1 = Class ((MSCng (F,s)),a) by A2, A4, EQREL_1:def_3;
reconsider a = a as Element of the Sorts of U1 . s by A5;
take y = (F . s) . a; ::_thesis: ( y in the Sorts of U2 . s & S1[x,y] )
thus  y in the Sorts of U2 . s ; ::_thesis: S1[x,y]
let b be Element of the Sorts of U1 . s; ::_thesis: ( x = Class ((MSCng (F,s)),b) implies y = (F . s) . b )
assume  x = Class ((MSCng (F,s)),b) ; ::_thesis: y = (F . s) . b
then  b in Class ((MSCng (F,s)),a) by A6, EQREL_1:23;
then  [b,a] in MSCng (F,s) by EQREL_1:19;
hence  y = (F . s) . b by Def17; ::_thesis: verum
end;
consider G being Function such that
A7: ( dom G = the Sorts of (QuotMSAlg (U1,(MSCng F))) . s & rng G c= the Sorts of U2 . s & ( for x being set st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds
S1[x,G . x] ) ) from FUNCT_1:sch_5(A3);
reconsider G = G as Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) by A7, FUNCT_2:def_1, RELSET_1:4;
take  G ; ::_thesis: for x being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),x)) = (F . s) . x
let a be Element of the Sorts of U1 . s; ::_thesis: G . (Class ((MSCng (F,s)),a)) = (F . s) . a
 Class ((MSCng (F,s)),a) in Class (MSCng (F,s)) by EQREL_1:def_3;
hence  G . (Class ((MSCng (F,s)),a)) = (F . s) . a by A2, A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) st ( for x being Element of the Sorts of U1 . s holds b1 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b2 . (Class ((MSCng (F,s)),x)) = (F . s) . x ) holds
b1 = b2
proof
set qa = QuotMSAlg (U1,(MSCng F));
set cqa = the Sorts of (QuotMSAlg (U1,(MSCng F)));
set u1 = the Sorts of U1;
set u2 = the Sorts of U2;
let H, G be Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s); ::_thesis: ( ( for x being Element of the Sorts of U1 . s holds H . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),x)) = (F . s) . x ) implies H = G )
assume that
A8: for a being Element of the Sorts of U1 . s holds H . (Class ((MSCng (F,s)),a)) = (F . s) . a and
A9: for a being Element of the Sorts of U1 . s holds G . (Class ((MSCng (F,s)),a)) = (F . s) . a ; ::_thesis: H = G
A10: the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) by Def6
.= Class (MSCng (F,s)) by A1, Def18 ;
 for x being set st x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s holds
H . x = G . x
proof
let x be set ; ::_thesis: ( x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s implies H . x = G . x )
assume A11: x in the Sorts of (QuotMSAlg (U1,(MSCng F))) . s ; ::_thesis: H . x = G . x
then reconsider x1 = x as Subset of ( the Sorts of U1 . s) by A10;
consider a being set  such that
A12: a in the Sorts of U1 . s and
A13: x1 = Class ((MSCng (F,s)),a) by A10, A11, EQREL_1:def_3;
reconsider a = a as Element of the Sorts of U1 . s by A12;
thus H . x = (F . s) . a by A8, A13
.= G . x by A9, A13 ; ::_thesis: verum
end;
hence  H = G by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines MSHomQuot MSUALG_4:def_19_:_
 for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S st F is_homomorphism U1,U2 holds
for b6 being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) holds
( b6 = MSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b6 . (Class ((MSCng (F,s)),x)) = (F . s) . x );

definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
func MSHomQuot F ->  ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 means :Def20: :: MSUALG_4:def 20
 for s being SortSymbol of S holds it . s = MSHomQuot (F,s);
existence
 ex b1 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st
for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s)
proof
deffunc H1( Element of S) ->  Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . $1),( the Sorts of U2 . $1) = MSHomQuot (F,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
 for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume  x in dom f ; ::_thesis: f . x is Function
then reconsider y = x as Element of S ;
 f . y = MSHomQuot (F,y) by A1;
hence  f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def_6;
 for i being set st i in the carrier of S holds
f . i is Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . i),( the Sorts of U2 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies f . i is Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . i),( the Sorts of U2 . i) )
assume  i in the carrier of S ; ::_thesis: f . i is Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . i),( the Sorts of U2 . i)
then reconsider s = i as Element of S ;
 f . s = MSHomQuot (F,s) by A1;
hence  f . i is Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . i),( the Sorts of U2 . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the Sorts of (QuotMSAlg (U1,(MSCng F))), the Sorts of U2 by PBOOLE:def_15;
reconsider f = f as ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 ;
take  f ; ::_thesis: for s being SortSymbol of S holds f . s = MSHomQuot (F,s)
thus  for s being SortSymbol of S holds f . s = MSHomQuot (F,s) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st ( for s being SortSymbol of S holds b1 . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds b2 . s = MSHomQuot (F,s) ) holds
b1 = b2
proof
let H, G be ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2; ::_thesis: ( ( for s being SortSymbol of S holds H . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds G . s = MSHomQuot (F,s) ) implies H = G )
assume that
A2: for s being SortSymbol of S holds H . s = MSHomQuot (F,s) and
A3: for s being SortSymbol of S holds G . s = MSHomQuot (F,s) ; ::_thesis: H = G
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
H_._i_=_G_._i
let i be set ; ::_thesis: ( i in the carrier of S implies H . i = G . i )
assume  i in the carrier of S ; ::_thesis: H . i = G . i
then reconsider s = i as SortSymbol of S ;
 H . s = MSHomQuot (F,s) by A2;
hence  H . i = G . i by A3; ::_thesis: verum
end;
hence  H = G by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def20 defines MSHomQuot MSUALG_4:def_20_:_
 for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for b5 being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 holds
( b5 = MSHomQuot F iff for s being SortSymbol of S holds b5 . s = MSHomQuot (F,s) );

theorem Th4: :: MSUALG_4:4
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 )
set mc = MSCng F;
set qa = QuotMSAlg (U1,(MSCng F));
set qh = MSHomQuot F;
set S1 = the Sorts of U1;
assume A1: F is_homomorphism U1,U2 ; ::_thesis: MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
 for o being OperSymbol of S st Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} holds
for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x)
proof
let o be OperSymbol of S; ::_thesis: ( Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} implies for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) )
assume  Args (o,(QuotMSAlg (U1,(MSCng F)))) <> {} ; ::_thesis: for x being Element of Args (o,(QuotMSAlg (U1,(MSCng F)))) holds ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x)
let x be Element of Args (o,(QuotMSAlg (U1,(MSCng F)))); ::_thesis: ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x)
set ro = the_result_sort_of o;
set ar = the_arity_of o;
A2: dom x = dom (the_arity_of o) by MSUALG_3:6;
 Args (o,(QuotMSAlg (U1,(MSCng F)))) = (((Class (MSCng F)) #) * the Arity of S) . o by MSUALG_1:def_4;
then consider a being Element of Args (o,U1) such that
A3: x = (MSCng F) # a by Th2;
A4: dom a = dom (the_arity_of o) by MSUALG_3:6;
A5: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_
((MSHomQuot_F)_#_x)_._y_=_(F_#_a)_._y
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((MSHomQuot F) # x) . y = (F # a) . y )
assume A6: y in dom (the_arity_of o) ; ::_thesis: ((MSHomQuot F) # x) . y = (F # a) . y
then reconsider n = y as Nat by ORDINAL1:def_12;
 (the_arity_of o) . n in rng (the_arity_of o) by A6, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . n as SortSymbol of S ;
A7: (the_arity_of o) /. n = (the_arity_of o) . n by A6, PARTFUN1:def_6;
then  x . n = Class (((MSCng F) . s),(a . n)) by A3, A6, Def7;
then A8: x . n = Class ((MSCng (F,s)),(a . n)) by A1, Def18;
A9: n in dom ( the Sorts of U1 * (the_arity_of o)) by A6, PARTFUN1:def_2;
then  a . n in ( the Sorts of U1 * (the_arity_of o)) . n by MSUALG_3:6;
then reconsider an = a . n as Element of the Sorts of U1 . s by A9, FUNCT_1:12;
((MSHomQuot F) # x) . n = ((MSHomQuot F) . s) . (x . n) by A2, A6, A7, MSUALG_3:def_6
.= (MSHomQuot (F,s)) . (x . n) by Def20
.= (F . s) . an by A1, A8, Def19
.= (F # a) . n by A4, A6, A7, MSUALG_3:def_6 ;
hence  ((MSHomQuot F) # x) . y = (F # a) . y ; ::_thesis: verum
end;
 o in the carrier' of S ;
then  o in dom ( the Sorts of U1 * the ResultSort of S) by PARTFUN1:def_2;
then A10: ( the Sorts of U1 * the ResultSort of S) . o = the Sorts of U1 . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then  ( rng (Den (o,U1)) c= Result (o,U1) & Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) ) by MSUALG_1:def_5;
then  rng (Den (o,U1)) c= dom (QuotRes ((MSCng F),o)) by A10, FUNCT_2:def_1;
then A11: ( dom (Den (o,U1)) = Args (o,U1) & dom ((QuotRes ((MSCng F),o)) * (Den (o,U1))) = dom (Den (o,U1)) ) by FUNCT_2:def_1, RELAT_1:27;
 the_arity_of o = the Arity of S . o by MSUALG_1:def_1;
then A12: product ((Class (MSCng F)) * (the_arity_of o)) = (((Class (MSCng F)) #) * the Arity of S) . o by MSAFREE:1;
reconsider da = (Den (o,U1)) . a as Element of the Sorts of U1 . (the_result_sort_of o) by A10, MSUALG_1:def_5;
A13: (MSHomQuot F) . (the_result_sort_of o) = MSHomQuot (F,(the_result_sort_of o)) by Def20;
Den (o,(QuotMSAlg (U1,(MSCng F)))) = (QuotCharact (MSCng F)) . o by MSUALG_1:def_6
.= QuotCharact ((MSCng F),o) by Def13 ;
then (Den (o,(QuotMSAlg (U1,(MSCng F))))) . x = ((QuotRes ((MSCng F),o)) * (Den (o,U1))) . a by A3, A12, Def12
.= (QuotRes ((MSCng F),o)) . da by A11, FUNCT_1:12
.= Class ((MSCng F),da) by Def8
.= Class ((MSCng (F,(the_result_sort_of o))),da) by A1, Def18 ;
then A14: ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (F . (the_result_sort_of o)) . ((Den (o,U1)) . a) by A1, A13, Def19
.= (Den (o,U2)) . (F # a) by A1, MSUALG_3:def_7 ;
 ( dom ((MSHomQuot F) # x) = dom (the_arity_of o) & dom (F # a) = dom (the_arity_of o) ) by MSUALG_3:6;
hence  ((MSHomQuot F) . (the_result_sort_of o)) . ((Den (o,(QuotMSAlg (U1,(MSCng F))))) . x) = (Den (o,U2)) . ((MSHomQuot F) # x) by A5, A14, FUNCT_1:2; ::_thesis: verum
end;
hence  MSHomQuot F is_homomorphism QuotMSAlg (U1,(MSCng F)),U2 by MSUALG_3:def_7; :: according to MSUALG_3:def_9 ::_thesis: MSHomQuot F is "1-1"
 for i being set st i in the carrier of S holds
(MSHomQuot F) . i is one-to-one
proof
let i be set ; ::_thesis: ( i in the carrier of S implies (MSHomQuot F) . i is one-to-one )
set f = (MSHomQuot F) . i;
assume  i in the carrier of S ; ::_thesis: (MSHomQuot F) . i is one-to-one
then reconsider s = i as SortSymbol of S ;
A15: (MSHomQuot F) . i = MSHomQuot (F,s) by Def20;
 for x1, x2 being set st x1 in dom ((MSHomQuot F) . i) & x2 in dom ((MSHomQuot F) . i) & ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom ((MSHomQuot F) . i) & x2 in dom ((MSHomQuot F) . i) & ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 implies x1 = x2 )
assume that
A16: x1 in dom ((MSHomQuot F) . i) and
A17: x2 in dom ((MSHomQuot F) . i) and
A18: ((MSHomQuot F) . i) . x1 = ((MSHomQuot F) . i) . x2 ; ::_thesis: x1 = x2
 x1 in (Class (MSCng F)) . s by A15, A16, FUNCT_2:def_1;
then  x1 in Class ((MSCng F) . s) by Def6;
then consider a1 being set  such that
A19: a1 in the Sorts of U1 . s and
A20: x1 = Class (((MSCng F) . s),a1) by EQREL_1:def_3;
 x2 in (Class (MSCng F)) . s by A15, A17, FUNCT_2:def_1;
then  x2 in Class ((MSCng F) . s) by Def6;
then consider a2 being set  such that
A21: a2 in the Sorts of U1 . s and
A22: x2 = Class (((MSCng F) . s),a2) by EQREL_1:def_3;
reconsider a2 = a2 as Element of the Sorts of U1 . s by A21;
A23: (MSCng F) . s = MSCng (F,s) by A1, Def18;
then A24: ((MSHomQuot F) . i) . x2 = (F . s) . a2 by A1, A15, A22, Def19;
reconsider a1 = a1 as Element of the Sorts of U1 . s by A19;
 ((MSHomQuot F) . i) . x1 = (F . s) . a1 by A1, A15, A23, A20, Def19;
then  [a1,a2] in MSCng (F,s) by A18, A24, Def17;
hence  x1 = x2 by A23, A20, A22, EQREL_1:35; ::_thesis: verum
end;
hence  (MSHomQuot F) . i is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
hence  MSHomQuot F is "1-1" by MSUALG_3:1; ::_thesis: verum
end;

theorem Th5: :: MSUALG_4:5
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 implies MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 )
set mc = MSCng F;
set qa = QuotMSAlg (U1,(MSCng F));
set qh = MSHomQuot F;
set Sq = the Sorts of (QuotMSAlg (U1,(MSCng F)));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
assume A1: F is_epimorphism U1,U2 ; ::_thesis: MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
then A2: F is_homomorphism U1,U2 by MSUALG_3:def_8;
A3: F is "onto" by A1, MSUALG_3:def_8;
 for i being set st i in the carrier of S holds
rng ((MSHomQuot F) . i) = the Sorts of U2 . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng ((MSHomQuot F) . i) = the Sorts of U2 . i )
set f = (MSHomQuot F) . i;
assume  i in the carrier of S ; ::_thesis: rng ((MSHomQuot F) . i) = the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
A4: rng (F . s) = the Sorts of U2 . s by A3, MSUALG_3:def_3;
A5: (MSHomQuot F) . i = MSHomQuot (F,s) by Def20;
hence  rng ((MSHomQuot F) . i) c= the Sorts of U2 . i by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of U2 . i c= rng ((MSHomQuot F) . i)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of U2 . i or x in rng ((MSHomQuot F) . i) )
assume  x in the Sorts of U2 . i ; ::_thesis: x in rng ((MSHomQuot F) . i)
then consider a being set  such that
A6: a in dom (F . s) and
A7: (F . s) . a = x by A4, FUNCT_1:def_3;
A8: ( MSCng (F,s) = (MSCng F) . s & the Sorts of (QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) ) by A2, Def6, Def18;
reconsider a = a as Element of the Sorts of U1 . s by A6;
 dom ((MSHomQuot F) . i) = the Sorts of (QuotMSAlg (U1,(MSCng F))) . s by A5, FUNCT_2:def_1;
then A9: Class ((MSCng (F,s)),a) in dom ((MSHomQuot F) . i) by A8, EQREL_1:def_3;
 ((MSHomQuot F) . i) . (Class ((MSCng (F,s)),a)) = x by A2, A5, A7, Def19;
hence  x in rng ((MSHomQuot F) . i) by A9, FUNCT_1:def_3; ::_thesis: verum
end;
then A10: MSHomQuot F is "onto" by MSUALG_3:def_3;
 MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2 by A2, Th4;
then  ( MSHomQuot F is_homomorphism QuotMSAlg (U1,(MSCng F)),U2 & MSHomQuot F is "1-1" ) by MSUALG_3:def_9;
hence  MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 by A10, MSUALG_3:13; ::_thesis: verum
end;

theorem :: MSUALG_4:6
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 implies QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic )
assume  F is_epimorphism U1,U2 ; ::_thesis: QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic
then  MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 by Th5;
hence  QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic by MSUALG_3:def_11; ::_thesis: verum
end;