:: by Ma{\l}gorzata Korolkiewicz

::

:: Received May 6, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

registration
end;

definition

let I be set ;

let A, B be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

b_{1} . i is Relation of (A . i),(B . i)

end;
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 for i being set st i in I holds

it . i is Relation of (A . i),(B . i);

ex b

for i being set st i in I holds

b

proof end;

:: deftheorem Def1 defines ManySortedRelation MSUALG_4:def 1 :

for I being set

for A, B, b_{4} being ManySortedSet of I holds

( b_{4} is ManySortedRelation of A,B iff for i being set st i in I holds

b_{4} . i is Relation of (A . i),(B . i) );

for I being set

for A, B, b

( b

b

registration

let I be set ;

let A, B be ManySortedSet of I;

coherence

for b_{1} being ManySortedRelation of A,B holds b_{1} is Relation-yielding

end;
let A, B be ManySortedSet of I;

coherence

for b

proof end;

definition

let I be set ;

let A be ManySortedSet of I;

mode ManySortedRelation of A is ManySortedRelation of A,A;

end;
let A be ManySortedSet of I;

mode ManySortedRelation of A is ManySortedRelation of A,A;

definition

let I be set ;

let A be ManySortedSet of I;

let IT be ManySortedRelation of A;

end;
let A be ManySortedSet of I;

let IT be ManySortedRelation of A;

attr IT 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);

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

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

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 func F . i -> Relation of (A . i),(B . i);

coherence

F . i is Relation of (A . i),(B . i) by Def1;

end;
let A, B be ManySortedSet of I;

let F be ManySortedRelation of A,B;

let i be Element of I;

:: original: .

redefine func F . i -> Relation of (A . i),(B . i);

coherence

F . i is Relation of (A . i),(B . i) by Def1;

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;
let U1 be MSAlgebra over S;

mode ManySortedRelation of U1 is ManySortedRelation of the Sorts of U1;

definition
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 );

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;

ex b_{1} being ManySortedRelation of U1 st b_{1} is MSEquivalence-like

end;
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 b

proof 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)

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

end;
let U1 be non-empty MSAlgebra over S;

let R be MSEquivalence-like ManySortedRelation of U1;

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

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;

ex b_{1} being MSEquivalence-like ManySortedRelation of U1 st b_{1} is MSCongruence-like

end;
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 b

proof 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;
let U1 be non-empty MSAlgebra over S;

mode MSCongruence of U1 is MSEquivalence-like MSCongruence-like ManySortedRelation of U1;

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 func R . i -> Equivalence_Relation of ( the Sorts of U1 . i);

coherence

R . i is Equivalence_Relation of ( the Sorts of U1 . i) by Th1;

end;
let U1 be MSAlgebra over S;

let R be MSEquivalence-like ManySortedRelation of U1;

let i be Element of S;

:: original: .

redefine func R . i -> Equivalence_Relation of ( the Sorts of U1 . i);

coherence

R . i is Equivalence_Relation of ( the Sorts of U1 . i) by Th1;

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;

correctness

coherence

Class ((R . i),x) is Subset of ( the Sorts of U1 . i);

;

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

correctness

coherence

Class ((R . i),x) is Subset of ( the Sorts of U1 . i);

;

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

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;

ex b_{1} being V8() ManySortedSet of the carrier of S st

for s being Element of S holds b_{1} . s = Class (R . s)

for b_{1}, b_{2} being V8() ManySortedSet of the carrier of S st ( for s being Element of S holds b_{1} . s = Class (R . s) ) & ( for s being Element of S holds b_{2} . s = Class (R . s) ) holds

b_{1} = b_{2}

end;
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 for s being Element of S holds it . s = Class (R . s);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being V8() ManySortedSet of the carrier of S holds

( b_{4} = Class R iff for s being Element of S holds b_{4} . s = Class (R . s) );

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for R being MSCongruence of U1

for b

( b

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 func F . o -> Function of (M1 . o),(M2 . o);

coherence

F . o is Function of (M1 . o),(M2 . o) by PBOOLE:def 15;

end;
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 func F . o -> Function of (M1 . o),(M2 . o);

coherence

F . o is Function of (M1 . o),(M2 . o) by PBOOLE:def 15;

registration

let I be non empty set ;

let p be FinSequence of I;

let X be ManySortedSet of I;

coherence

for b_{1} being Function st b_{1} = X * p holds

b_{1} is dom p -defined

end;
let p be FinSequence of I;

let X be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be non empty set ;

let p be FinSequence of I;

let X be ManySortedSet of I;

coherence

for b_{1} being dom p -defined Function st b_{1} = X * p holds

b_{1} is total

end;
let p be FinSequence of I;

let X be ManySortedSet of I;

coherence

for b

b

proof 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);

ex b_{1} being Element of product ((Class R) * (the_arity_of o)) st

for n being Nat st n in dom (the_arity_of o) holds

b_{1} . n = Class ((R . ((the_arity_of o) /. n)),(x . n))

for b_{1}, b_{2} being Element of product ((Class R) * (the_arity_of o)) st ( for n being Nat st n in dom (the_arity_of o) holds

b_{1} . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) & ( for n being Nat st n in dom (the_arity_of o) holds

b_{2} . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) ) holds

b_{1} = b_{2}

end;
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);

func R # 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 for n being Nat st n in dom (the_arity_of o) holds

it . n = Class ((R . ((the_arity_of o) /. n)),(x . n));

ex b

for n being Nat st n in dom (the_arity_of o) holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{6} being Element of product ((Class R) * (the_arity_of o)) holds

( b_{6} = R # x iff for n being Nat st n in dom (the_arity_of o) holds

b_{6} . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) );

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 b

( b

b

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;

ex b_{1} 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 b_{1} . x = Class (R,x)

for b_{1}, b_{2} 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 b_{1} . x = Class (R,x) ) & ( for x being Element of the Sorts of A . (the_result_sort_of o) holds b_{2} . x = Class (R,x) ) holds

b_{1} = b_{2}

ex b_{1} 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 b_{1} . x = R # x

for b_{1}, b_{2} 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 b_{1} . x = R # x ) & ( for x being Element of Args (o,A) holds b_{2} . x = R # x ) holds

b_{1} = b_{2}

end;
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 for x being Element of the Sorts of A . (the_result_sort_of o) holds it . x = Class (R,x);

ex b

for x being Element of the Sorts of A . (the_result_sort_of o) holds b

proof end;

uniqueness for b

b

proof 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 for x being Element of Args (o,A) holds it . x = R # x;

ex b

for x being Element of Args (o,A) holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) holds

( b_{5} = QuotRes (R,o) iff for x being Element of the Sorts of A . (the_result_sort_of o) holds b_{5} . x = Class (R,x) );

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 b

( b

:: 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 b_{5} being Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) holds

( b_{5} = QuotArgs (R,o) iff for x being Element of Args (o,A) holds b_{5} . x = R # x );

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 b

( b

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be MSCongruence of A;

ex b_{1} 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 b_{1} . o = QuotRes (R,o)

for b_{1}, b_{2} 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 b_{1} . o = QuotRes (R,o) ) & ( for o being OperSymbol of S holds b_{2} . o = QuotRes (R,o) ) holds

b_{1} = b_{2}

ex b_{1} 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 b_{1} . o = QuotArgs (R,o)

for b_{1}, b_{2} 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 b_{1} . o = QuotArgs (R,o) ) & ( for o being OperSymbol of S holds b_{2} . o = QuotArgs (R,o) ) holds

b_{1} = b_{2}

end;
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 for o being OperSymbol of S holds it . o = QuotRes (R,o);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof 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 for o being OperSymbol of S holds it . o = QuotArgs (R,o);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being ManySortedFunction of the Sorts of A * the ResultSort of S,(Class R) * the ResultSort of S holds

( b_{4} = QuotRes R iff for o being OperSymbol of S holds b_{4} . o = QuotRes (R,o) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being MSCongruence of A

for b

( b

:: 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 b_{4} being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S holds

( b_{4} = QuotArgs R iff for o being OperSymbol of S holds b_{4} . o = QuotArgs (R,o) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being MSCongruence of A

for b

( b

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

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

ex b_{1} 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

b_{1} . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a ) holds

b_{1} = b_{2}

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

ex b

for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being Function of ((((Class R) #) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o) holds

( b_{5} = QuotCharact (R,o) iff for a being Element of Args (o,A) st R # a in (((Class R) #) * the Arity of S) . o holds

b_{5} . (R # a) = ((QuotRes (R,o)) * (Den (o,A))) . a );

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 b

( b

b

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let R be MSCongruence of A;

ex b_{1} being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st

for o being OperSymbol of S holds b_{1} . o = QuotCharact (R,o)

for b_{1}, b_{2} being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S st ( for o being OperSymbol of S holds b_{1} . o = QuotCharact (R,o) ) & ( for o being OperSymbol of S holds b_{2} . o = QuotCharact (R,o) ) holds

b_{1} = b_{2}

end;
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 for o being OperSymbol of S holds it . o = QuotCharact (R,o);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being ManySortedFunction of ((Class R) #) * the Arity of S,(Class R) * the ResultSort of S holds

( b_{4} = QuotCharact R iff for o being OperSymbol of S holds b_{4} . o = QuotCharact (R,o) );

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being MSCongruence of A

for b

( b

definition

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

let R be MSCongruence of U1;

MSAlgebra(# (Class R),(QuotCharact R) #) is MSAlgebra over S ;

end;
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) #);

MSAlgebra(# (Class R),(QuotCharact R) #) is MSAlgebra over S ;

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

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;

coherence

( QuotMSAlg (U1,R) is strict & QuotMSAlg (U1,R) is non-empty ) by MSUALG_1:def 3;

end;
let U1 be non-empty MSAlgebra over S;

let R be MSCongruence of U1;

coherence

( QuotMSAlg (U1,R) is strict & QuotMSAlg (U1,R) is non-empty ) by MSUALG_1:def 3;

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;

ex b_{1} 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

b_{1} . x = Class ((R . s),x)

for b_{1}, b_{2} 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

b_{1} . x = Class ((R . s),x) ) & ( for x being set st x in the Sorts of U1 . s holds

b_{2} . x = Class ((R . s),x) ) holds

b_{1} = b_{2}

end;
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 for x being set st x in the Sorts of U1 . s holds

it . x = Class ((R . s),x);

ex b

for x being set st x in the Sorts of U1 . s holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being Function of ( the Sorts of U1 . s),((Class R) . s) holds

( b_{5} = MSNat_Hom (U1,R,s) iff for x being set st x in the Sorts of U1 . s holds

b_{5} . x = Class ((R . s),x) );

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 b

( b

b

definition

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

let R be MSCongruence of U1;

ex b_{1} being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st

for s being SortSymbol of S holds b_{1} . s = MSNat_Hom (U1,R,s)

for b_{1}, b_{2} being ManySortedFunction of U1,(QuotMSAlg (U1,R)) st ( for s being SortSymbol of S holds b_{1} . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds b_{2} . s = MSNat_Hom (U1,R,s) ) holds

b_{1} = b_{2}

end;
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 for s being SortSymbol of S holds it . s = MSNat_Hom (U1,R,s);

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being ManySortedFunction of U1,(QuotMSAlg (U1,R)) holds

( b_{4} = MSNat_Hom (U1,R) iff for s being SortSymbol of S holds b_{4} . s = MSNat_Hom (U1,R,s) );

for S being non empty non void ManySortedSign

for U1 being non-empty MSAlgebra over S

for R being MSCongruence of U1

for b

( b

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)

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

ex b_{1} 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 b_{1} iff (F . s) . x = (F . s) . y )

for b_{1}, b_{2} 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 b_{1} iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds

( [x,y] in b_{2} iff (F . s) . x = (F . s) . y ) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of the Sorts of U1 . s holds

( [x,y] in it iff (F . s) . x = (F . s) . y );

ex b

for x, y being Element of the Sorts of U1 . s holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof 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 b_{6} being Equivalence_Relation of ( the Sorts of U1 . s) holds

( b_{6} = MSCng (F,s) iff for x, y being Element of the Sorts of U1 . s holds

( [x,y] in b_{6} iff (F . s) . x = (F . s) . y ) );

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 b

( b

( [x,y] in b

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 ;

ex b_{1} being MSCongruence of U1 st

for s being SortSymbol of S holds b_{1} . s = MSCng (F,s)

for b_{1}, b_{2} being MSCongruence of U1 st ( for s being SortSymbol of S holds b_{1} . s = MSCng (F,s) ) & ( for s being SortSymbol of S holds b_{2} . s = MSCng (F,s) ) holds

b_{1} = b_{2}

end;
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 for s being SortSymbol of S holds it . s = MSCng (F,s);

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being MSCongruence of U1 holds

( b_{5} = MSCng F iff for s being SortSymbol of S holds b_{5} . s = MSCng (F,s) );

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 b

( b

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 ;

ex b_{1} 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 b_{1} . (Class ((MSCng (F,s)),x)) = (F . s) . x

for b_{1}, b_{2} 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 b_{1} . (Class ((MSCng (F,s)),x)) = (F . s) . x ) & ( for x being Element of the Sorts of U1 . s holds b_{2} . (Class ((MSCng (F,s)),x)) = (F . s) . x ) holds

b_{1} = b_{2}

end;
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 for x being Element of the Sorts of U1 . s holds it . (Class ((MSCng (F,s)),x)) = (F . s) . x;

ex b

for x being Element of the Sorts of U1 . s holds b

proof end;

uniqueness for b

b

proof 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 b_{6} being Function of ( the Sorts of (QuotMSAlg (U1,(MSCng F))) . s),( the Sorts of U2 . s) holds

( b_{6} = MSHomQuot (F,s) iff for x being Element of the Sorts of U1 . s holds b_{6} . (Class ((MSCng (F,s)),x)) = (F . s) . x );

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 b

( b

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;

ex b_{1} being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st

for s being SortSymbol of S holds b_{1} . s = MSHomQuot (F,s)

for b_{1}, b_{2} being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 st ( for s being SortSymbol of S holds b_{1} . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds b_{2} . s = MSHomQuot (F,s) ) holds

b_{1} = b_{2}

end;
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 for s being SortSymbol of S holds it . s = MSHomQuot (F,s);

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2 holds

( b_{5} = MSHomQuot F iff for s being SortSymbol of S holds b_{5} . s = MSHomQuot (F,s) );

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 b

( b

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

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

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

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