:: ALG_1 semantic presentation

begin


theorem Th1: :: ALG_1:1
for U1 being Universal_Algebra
for B being non empty Subset of U1 st B = the carrier of U1 holds
Opers (U1,B) = the charact of U1
proof
let U1 be Universal_Algebra; ::_thesis: for B being non empty Subset of U1 st B = the carrier of U1 holds
Opers (U1,B) = the charact of U1
let B be non empty Subset of U1; ::_thesis: ( B = the carrier of U1 implies Opers (U1,B) = the charact of U1 )
A1: dom (Opers (U1,B)) = dom the charact of U1 by UNIALG_2:def_6;
assume A2: B = the carrier of U1 ; ::_thesis: Opers (U1,B) = the charact of U1
now__::_thesis:_for_n_being_Nat_st_n_in_dom_the_charact_of_U1_holds_
(Opers_(U1,B))_._n_=_the_charact_of_U1_._n
let n be Nat; ::_thesis: ( n in dom the charact of U1 implies (Opers (U1,B)) . n = the charact of U1 . n )
assume A3: n in dom the charact of U1 ; ::_thesis: (Opers (U1,B)) . n = the charact of U1 . n
then reconsider o = the charact of U1 . n as operation of U1 by FUNCT_1:def_3;
thus (Opers (U1,B)) . n = o /. B by A1, A3, UNIALG_2:def_6
.= the charact of U1 . n by A2, UNIALG_2:4 ; ::_thesis: verum
end;
hence  Opers (U1,B) = the charact of U1 by A1, FINSEQ_1:13; ::_thesis: verum
end;


theorem :: ALG_1:2
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds f * (<*> the carrier of U1) = <*> the carrier of U2 ;

theorem Th3: :: ALG_1:3
for U1 being Universal_Algebra
for a being FinSequence of U1 holds (id the carrier of U1) * a = a
proof
let U1 be Universal_Algebra; ::_thesis: for a being FinSequence of U1 holds (id the carrier of U1) * a = a
let a be FinSequence of U1; ::_thesis: (id the carrier of U1) * a = a
set f = id the carrier of U1;
A1: dom ((id the carrier of U1) * a) = dom a by FINSEQ_3:120;
A2: now__::_thesis:_for_n_being_Nat_st_n_in_dom_((id_the_carrier_of_U1)_*_a)_holds_
((id_the_carrier_of_U1)_*_a)_._n_=_a_._n
let n be Nat; ::_thesis: ( n in dom ((id the carrier of U1) * a) implies ((id the carrier of U1) * a) . n = a . n )
assume A3: n in dom ((id the carrier of U1) * a) ; ::_thesis: ((id the carrier of U1) * a) . n = a . n
then reconsider u = a . n as Element of U1 by A1, FINSEQ_2:11;
 (id the carrier of U1) . u = u by FUNCT_1:18;
hence  ((id the carrier of U1) * a) . n = a . n by A3, FINSEQ_3:120; ::_thesis: verum
end;
 len ((id the carrier of U1) * a) = len a by FINSEQ_3:120;
hence  (id the carrier of U1) * a = a by A2, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th4: :: ALG_1:4
for U1, U2, U3 being Universal_Algebra
for h1 being Function of U1,U2
for h2 being Function of U2,U3
for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
proof
let U1, U2, U3 be Universal_Algebra; ::_thesis: for h1 being Function of U1,U2
for h2 being Function of U2,U3
for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
let h1 be Function of U1,U2; ::_thesis: for h2 being Function of U2,U3
for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
let h2 be Function of U2,U3; ::_thesis: for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
let a be FinSequence of U1; ::_thesis: h2 * (h1 * a) = (h2 * h1) * a
A1: dom a = Seg (len a) by FINSEQ_1:def_3;
A2: dom (h2 * (h1 * a)) = dom (h1 * a) by FINSEQ_3:120;
 dom (h1 * a) = dom a by FINSEQ_3:120;
then A3: dom (h2 * (h1 * a)) = Seg (len a) by A2, FINSEQ_1:def_3;
A4: len a = len ((h2 * h1) * a) by FINSEQ_3:120;
then A5: dom ((h2 * h1) * a) = Seg (len a) by FINSEQ_1:def_3;
A6: now__::_thesis:_for_n_being_Nat_st_n_in_dom_(h2_*_(h1_*_a))_holds_
(h2_*_(h1_*_a))_._n_=_((h2_*_h1)_*_a)_._n
let n be Nat; ::_thesis: ( n in dom (h2 * (h1 * a)) implies (h2 * (h1 * a)) . n = ((h2 * h1) * a) . n )
assume A7: n in dom (h2 * (h1 * a)) ; ::_thesis: (h2 * (h1 * a)) . n = ((h2 * h1) * a) . n
hence (h2 * (h1 * a)) . n = h2 . ((h1 * a) . n) by FINSEQ_3:120
.= h2 . (h1 . (a . n)) by A2, A7, FINSEQ_3:120
.= (h2 * h1) . (a . n) by A1, A3, A7, FINSEQ_2:11, FUNCT_2:15
.= ((h2 * h1) * a) . n by A3, A5, A7, FINSEQ_3:120 ;
::_thesis: verum
end;
 ( len (h2 * (h1 * a)) = len (h1 * a) & len (h1 * a) = len a ) by FINSEQ_3:120;
hence  h2 * (h1 * a) = (h2 * h1) * a by A4, A6, FINSEQ_2:9; ::_thesis: verum
end;

definition
let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
predf is_homomorphism U1,U2 means :Def1: :: ALG_1:def 1
( U1,U2 are_similar & ( for n being Element of NAT st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = the charact of U1 . n & o2 = the charact of U2 . n holds
for x being FinSequence of U1 st x in dom o1 holds
f . (o1 . x) = o2 . (f * x) ) );
end;

:: deftheorem Def1 defines is_homomorphism ALG_1:def_1_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_homomorphism U1,U2 iff ( U1,U2 are_similar & ( for n being Element of NAT st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of U2 st o1 = the charact of U1 . n & o2 = the charact of U2 . n holds
for x being FinSequence of U1 st x in dom o1 holds
f . (o1 . x) = o2 . (f * x) ) ) );

definition
let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
predf is_monomorphism U1,U2 means :Def2: :: ALG_1:def 2
( f is_homomorphism U1,U2 & f is one-to-one );
predf is_epimorphism U1,U2 means :Def3: :: ALG_1:def 3
( f is_homomorphism U1,U2 & rng f = the carrier of U2 );
end;

:: deftheorem Def2 defines is_monomorphism ALG_1:def_2_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_monomorphism U1,U2 iff ( f is_homomorphism U1,U2 & f is one-to-one ) );

:: deftheorem Def3 defines is_epimorphism ALG_1:def_3_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_epimorphism U1,U2 iff ( f is_homomorphism U1,U2 & rng f = the carrier of U2 ) );

definition
let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
predf is_isomorphism U1,U2 means :Def4: :: ALG_1:def 4
( f is_monomorphism U1,U2 & f is_epimorphism U1,U2 );
end;

:: deftheorem Def4 defines is_isomorphism ALG_1:def_4_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_isomorphism U1,U2 iff ( f is_monomorphism U1,U2 & f is_epimorphism U1,U2 ) );

definition
let U1, U2 be Universal_Algebra;
predU1,U2 are_isomorphic  means :Def5: :: ALG_1:def 5
 ex f being Function of U1,U2 st f is_isomorphism U1,U2;
end;

:: deftheorem Def5 defines are_isomorphic ALG_1:def_5_:_
 for U1, U2 being Universal_Algebra holds
( U1,U2 are_isomorphic iff ex f being Function of U1,U2 st f is_isomorphism U1,U2 );

theorem Th5: :: ALG_1:5
for U1 being Universal_Algebra holds id the carrier of U1 is_homomorphism U1,U1
proof
let U1 be Universal_Algebra; ::_thesis: id the carrier of U1 is_homomorphism U1,U1
thus  U1,U1 are_similar ; :: according to ALG_1:def_1 ::_thesis: for n being Element of NAT st n in dom the charact of U1 holds
for o1, o2 being operation of U1 st o1 = the charact of U1 . n & o2 = the charact of U1 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
let n be Element of NAT ; ::_thesis: ( n in dom the charact of U1 implies for o1, o2 being operation of U1 st o1 = the charact of U1 . n & o2 = the charact of U1 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) )
assume  n in dom the charact of U1 ; ::_thesis: for o1, o2 being operation of U1 st o1 = the charact of U1 . n & o2 = the charact of U1 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
let o1, o2 be operation of U1; ::_thesis: ( o1 = the charact of U1 . n & o2 = the charact of U1 . n implies for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) )
assume A1: ( o1 = the charact of U1 . n & o2 = the charact of U1 . n ) ; ::_thesis: for x being FinSequence of U1 st x in dom o1 holds
(id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
set f = id the carrier of U1;
let x be FinSequence of U1; ::_thesis: ( x in dom o1 implies (id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) )
assume  x in dom o1 ; ::_thesis: (id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x)
then  o1 . x in rng o1 by FUNCT_1:def_3;
then reconsider u = o1 . x as Element of U1 ;
 (id the carrier of U1) . u = u by FUNCT_1:18;
hence  (id the carrier of U1) . (o1 . x) = o2 . ((id the carrier of U1) * x) by A1, Th3; ::_thesis: verum
end;

theorem Th6: :: ALG_1:6
for U1, U2, U3 being Universal_Algebra
for h1 being Function of U1,U2
for h2 being Function of U2,U3 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3
proof
let U1, U2, U3 be Universal_Algebra; ::_thesis: for h1 being Function of U1,U2
for h2 being Function of U2,U3 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3
let h1 be Function of U1,U2; ::_thesis: for h2 being Function of U2,U3 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3
let h2 be Function of U2,U3; ::_thesis: ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 implies h2 * h1 is_homomorphism U1,U3 )
set s1 = signature U1;
set s2 = signature U2;
set s3 = signature U3;
assume that
A1: h1 is_homomorphism U1,U2 and
A2: h2 is_homomorphism U2,U3 ; ::_thesis: h2 * h1 is_homomorphism U1,U3
 U1,U2 are_similar by A1, Def1;
then A3: signature U1 = signature U2 by UNIALG_2:def_1;
 U2,U3 are_similar by A2, Def1;
hence  signature U1 = signature U3 by A3, UNIALG_2:def_1; :: according to UNIALG_2:def_1,ALG_1:def_1 ::_thesis: for n being Element of NAT st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x)
let n be Element of NAT ; ::_thesis: ( n in dom the charact of U1 implies for o1 being operation of U1
for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x) )
assume A4: n in dom the charact of U1 ; ::_thesis: for o1 being operation of U1
for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x)
let o1 be operation of U1; ::_thesis: for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x)
let o3 be operation of U3; ::_thesis: ( o1 = the charact of U1 . n & o3 = the charact of U3 . n implies for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o3 . ((h2 * h1) * x) )
assume that
A5: o1 = the charact of U1 . n and
A6: o3 = the charact of U3 . n ; ::_thesis: for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o3 . ((h2 * h1) * x)
let a be FinSequence of U1; ::_thesis: ( a in dom o1 implies (h2 * h1) . (o1 . a) = o3 . ((h2 * h1) * a) )
reconsider b = h1 * a as Element of the carrier of U2 * by FINSEQ_1:def_11;
assume A7: a in dom o1 ; ::_thesis: (h2 * h1) . (o1 . a) = o3 . ((h2 * h1) * a)
then A8: o1 . a in rng o1 by FUNCT_1:def_3;
 dom o1 = (arity o1) -tuples_on the carrier of U1 by MARGREL1:22;
then  a in  {  w where w is Element of the carrier of U1 * : len w = arity o1  }  by A7, FINSEQ_2:def_4;
then A9: ex w being Element of the carrier of U1 * st
( w = a & len w = arity o1 ) ;
A10: ( len (signature U1) = len the charact of U1 & dom the charact of U1 = Seg (len the charact of U1) ) by FINSEQ_1:def_3, UNIALG_1:def_4;
A11: ( len (signature U2) = len the charact of U2 & dom the charact of U2 = Seg (len the charact of U2) ) by FINSEQ_1:def_3, UNIALG_1:def_4;
then reconsider o2 = the charact of U2 . n as operation of U2 by A3, A10, A4, FUNCT_1:def_3;
A12: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3;
then A13: (signature U2) . n = arity o2 by A3, A10, A4, UNIALG_1:def_4;
 (signature U1) . n = arity o1 by A10, A12, A4, A5, UNIALG_1:def_4;
then  len (h1 * a) = arity o2 by A3, A13, A9, FINSEQ_3:120;
then  ( dom o2 = (arity o2) -tuples_on the carrier of U2 & b in  {  s where s is Element of the carrier of U2 * : len s = arity o2  }  ) by MARGREL1:22;
then  h1 * a in dom o2 by FINSEQ_2:def_4;
then A14: h2 . (o2 . (h1 * a)) = o3 . (h2 * (h1 * a)) by A2, A3, A10, A11, A4, A6, Def1;
 h1 . (o1 . a) = o2 . (h1 * a) by A1, A4, A5, A7, Def1;
hence (h2 * h1) . (o1 . a) = o3 . (h2 * (h1 * a)) by A8, A14, FUNCT_2:15
.= o3 . ((h2 * h1) * a) by Th4 ;
::_thesis: verum
end;

theorem Th7: :: ALG_1:7
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 holds
( f is_isomorphism U1,U2 iff ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one ) )
proof
let U1, U2 be Universal_Algebra; ::_thesis: for f being Function of U1,U2 holds
( f is_isomorphism U1,U2 iff ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one ) )
let f be Function of U1,U2; ::_thesis: ( f is_isomorphism U1,U2 iff ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one ) )
thus  ( f is_isomorphism U1,U2 implies ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one ) ) ::_thesis: ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one implies f is_isomorphism U1,U2 )
proof
assume  f is_isomorphism U1,U2 ; ::_thesis: ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one )
then  ( f is_monomorphism U1,U2 & f is_epimorphism U1,U2 ) by Def4;
hence  ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one ) by Def2, Def3; ::_thesis: verum
end;
assume  ( f is_homomorphism U1,U2 & rng f = the carrier of U2 & f is one-to-one ) ; ::_thesis: f is_isomorphism U1,U2
then  ( f is_monomorphism U1,U2 & f is_epimorphism U1,U2 ) by Def2, Def3;
hence  f is_isomorphism U1,U2 by Def4; ::_thesis: verum
end;

theorem Th8: :: ALG_1:8
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_isomorphism U1,U2 holds
( dom f = the carrier of U1 & rng f = the carrier of U2 )
proof
let U1, U2 be Universal_Algebra; ::_thesis: for f being Function of U1,U2 st f is_isomorphism U1,U2 holds
( dom f = the carrier of U1 & rng f = the carrier of U2 )
let f be Function of U1,U2; ::_thesis: ( f is_isomorphism U1,U2 implies ( dom f = the carrier of U1 & rng f = the carrier of U2 ) )
assume  f is_isomorphism U1,U2 ; ::_thesis: ( dom f = the carrier of U1 & rng f = the carrier of U2 )
then  f is_epimorphism U1,U2 by Def4;
hence  ( dom f = the carrier of U1 & rng f = the carrier of U2 ) by Def3, FUNCT_2:def_1; ::_thesis: verum
end;

theorem Th9: :: ALG_1:9
for U1, U2 being Universal_Algebra
for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_homomorphism U2,U1
proof
let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_homomorphism U2,U1
let h be Function of U1,U2; ::_thesis: for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_homomorphism U2,U1
let h1 be Function of U2,U1; ::_thesis: ( h is_isomorphism U1,U2 & h1 = h " implies h1 is_homomorphism U2,U1 )
assume that
A1: h is_isomorphism U1,U2 and
A2: h1 = h " ; ::_thesis: h1 is_homomorphism U2,U1
A3: h is one-to-one by A1, Th7;
A4: h is_homomorphism U1,U2 by A1, Th7;
then A5: U1,U2 are_similar by Def1;
then A6: signature U1 = signature U2 by UNIALG_2:def_1;
A7: ( len (signature U1) = len the charact of U1 & dom the charact of U1 = Seg (len the charact of U1) ) by FINSEQ_1:def_3, UNIALG_1:def_4;
A8: dom (signature U2) = Seg (len (signature U2)) by FINSEQ_1:def_3;
A9: ( len (signature U2) = len the charact of U2 & dom the charact of U2 = Seg (len the charact of U2) ) by FINSEQ_1:def_3, UNIALG_1:def_4;
A10: rng h = the carrier of U2 by A1, Th7;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_the_charact_of_U2_holds_
for_o2_being_operation_of_U2
for_o1_being_operation_of_U1_st_o2_=_the_charact_of_U2_._n_&_o1_=_the_charact_of_U1_._n_holds_
for_x_being_FinSequence_of_U2_st_x_in_dom_o2_holds_
h1_._(o2_._x)_=_o1_._(h1_*_x)
let n be Element of NAT ; ::_thesis: ( n in dom the charact of U2 implies for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x) )
assume A11: n in dom the charact of U2 ; ::_thesis: for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)
let o2 be operation of U2; ::_thesis: for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)
let o1 be operation of U1; ::_thesis: ( o2 = the charact of U2 . n & o1 = the charact of U1 . n implies for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x) )
assume A12: ( o2 = the charact of U2 . n & o1 = the charact of U1 . n ) ; ::_thesis: for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)
let x be FinSequence of U2; ::_thesis: ( x in dom o2 implies h1 . (o2 . x) = o1 . (h1 * x) )
defpred S1[ set , set ] means h . $2 = x . $1;
A13: dom x = Seg (len x) by FINSEQ_1:def_3;
A14: for m being Nat st m in Seg (len x) holds
ex a being Element of U1 st S1[m,a]
proof
let m be Nat; ::_thesis: ( m in Seg (len x) implies ex a being Element of U1 st S1[m,a] )
assume  m in Seg (len x) ; ::_thesis: ex a being Element of U1 st S1[m,a]
then  m in dom x by FINSEQ_1:def_3;
then  x . m in the carrier of U2 by FINSEQ_2:11;
then consider a being set  such that
A15: a in dom h and
A16: h . a = x . m by A10, FUNCT_1:def_3;
reconsider a = a as Element of U1 by A15;
take  a ; ::_thesis: S1[m,a]
thus  S1[m,a] by A16; ::_thesis: verum
end;
consider p being FinSequence of U1 such that
A17: ( dom p = Seg (len x) & ( for m being Nat st m in Seg (len x) holds
S1[m,p . m] ) ) from FINSEQ_1:sch_5(A14);
A18: dom (h * p) = dom p by FINSEQ_3:120;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_
x_._n_=_(h_*_p)_._n
let n be Nat; ::_thesis: ( n in dom x implies x . n = (h * p) . n )
assume A19: n in dom x ; ::_thesis: x . n = (h * p) . n
hence x . n = h . (p . n) by A17, A13
.= (h * p) . n by A17, A13, A18, A19, FINSEQ_3:120 ;
::_thesis: verum
end;
then A20: x = h * p by A17, A13, A18, FINSEQ_1:13;
A21: len p = len x by A17, FINSEQ_1:def_3;
assume  x in dom o2 ; ::_thesis: h1 . (o2 . x) = o1 . (h1 * x)
then  x in (arity o2) -tuples_on the carrier of U2 by MARGREL1:22;
then  x in  {  s where s is Element of the carrier of U2 * : len s = arity o2  }  by FINSEQ_2:def_4;
then A22: ex s being Element of the carrier of U2 * st
( x = s & len s = arity o2 ) ;
A23: h1 * h = id (dom h) by A2, A3, FUNCT_1:39
.= id the carrier of U1 by FUNCT_2:def_1 ;
then A24: h1 * x = (id the carrier of U1) * p by A20, Th4
.= p by Th3 ;
reconsider p = p as Element of the carrier of U1 * by FINSEQ_1:def_11;
 ( (signature U1) . n = arity o1 & (signature U2) . n = arity o2 ) by A6, A8, A9, A11, A12, UNIALG_1:def_4;
then  p in  {  w where w is Element of the carrier of U1 * : len w = arity o1  }  by A6, A22, A21;
then  p in (arity o1) -tuples_on the carrier of U1 by FINSEQ_2:def_4;
then A25: p in dom o1 by MARGREL1:22;
then A26: h1 . (o2 . x) = h1 . (h . (o1 . p)) by A4, A6, A7, A9, A11, A12, A20, Def1;
A27: o1 . p in the carrier of U1 by A25, PARTFUN1:4;
then  o1 . p in dom h by FUNCT_2:def_1;
hence h1 . (o2 . x) = (id the carrier of U1) . (o1 . p) by A23, A26, FUNCT_1:13
.= o1 . (h1 * x) by A24, A27, FUNCT_1:17 ;
::_thesis: verum
end;
hence  h1 is_homomorphism U2,U1 by A5, Def1; ::_thesis: verum
end;

theorem Th10: :: ALG_1:10
for U1, U2 being Universal_Algebra
for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_isomorphism U2,U1
proof
let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_isomorphism U2,U1
let h be Function of U1,U2; ::_thesis: for h1 being Function of U2,U1 st h is_isomorphism U1,U2 & h1 = h " holds
h1 is_isomorphism U2,U1
let h1 be Function of U2,U1; ::_thesis: ( h is_isomorphism U1,U2 & h1 = h " implies h1 is_isomorphism U2,U1 )
assume that
A1: h is_isomorphism U1,U2 and
A2: h1 = h " ; ::_thesis: h1 is_isomorphism U2,U1
A3: h1 is_homomorphism U2,U1 by A1, A2, Th9;
A4: h is one-to-one by A1, Th7;
then  rng h1 = dom h by A2, FUNCT_1:33
.= the carrier of U1 by FUNCT_2:def_1 ;
hence  h1 is_isomorphism U2,U1 by A2, A4, A3, Th7; ::_thesis: verum
end;

theorem Th11: :: ALG_1:11
for U1, U2, U3 being Universal_Algebra
for h being Function of U1,U2
for h1 being Function of U2,U3 st h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 holds
h1 * h is_isomorphism U1,U3
proof
let U1, U2, U3 be Universal_Algebra; ::_thesis: for h being Function of U1,U2
for h1 being Function of U2,U3 st h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 holds
h1 * h is_isomorphism U1,U3
let h be Function of U1,U2; ::_thesis: for h1 being Function of U2,U3 st h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 holds
h1 * h is_isomorphism U1,U3
let h1 be Function of U2,U3; ::_thesis: ( h is_isomorphism U1,U2 & h1 is_isomorphism U2,U3 implies h1 * h is_isomorphism U1,U3 )
assume that
A1: h is_isomorphism U1,U2 and
A2: h1 is_isomorphism U2,U3 ; ::_thesis: h1 * h is_isomorphism U1,U3
 ( dom h1 = the carrier of U2 & rng h = the carrier of U2 ) by A1, Th8, FUNCT_2:def_1;
then A3: rng (h1 * h) = rng h1 by RELAT_1:28
.= the carrier of U3 by A2, Th8 ;
 ( h is_homomorphism U1,U2 & h1 is_homomorphism U2,U3 ) by A1, A2, Th7;
then A4: h1 * h is_homomorphism U1,U3 by Th6;
 ( h is one-to-one & h1 is one-to-one ) by A1, A2, Th7;
hence  h1 * h is_isomorphism U1,U3 by A3, A4, Th7; ::_thesis: verum
end;

theorem :: ALG_1:12
for U1 being Universal_Algebra holds U1,U1 are_isomorphic
proof
let U1 be Universal_Algebra; ::_thesis: U1,U1 are_isomorphic
set i = id the carrier of U1;
 ( id the carrier of U1 is_homomorphism U1,U1 & rng (id the carrier of U1) = the carrier of U1 ) by Th5;
then  id the carrier of U1 is_isomorphism U1,U1 by Th7;
hence  U1,U1 are_isomorphic by Def5; ::_thesis: verum
end;

theorem :: ALG_1:13
for U1, U2 being Universal_Algebra st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic
proof
let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_isomorphic implies U2,U1 are_isomorphic )
assume  U1,U2 are_isomorphic ; ::_thesis: U2,U1 are_isomorphic
then consider f being Function of U1,U2 such that
A1: f is_isomorphism U1,U2 by Def5;
 f is_monomorphism U1,U2 by A1, Def4;
then A2: f is one-to-one by Def2;
then A3: rng (f ") = dom f by FUNCT_1:33
.= the carrier of U1 by FUNCT_2:def_1 ;
A4: f is_epimorphism U1,U2 by A1, Def4;
dom (f ") = rng f by A2, FUNCT_1:33
.= the carrier of U2 by A4, Def3 ;
then reconsider g = f " as Function of U2,U1 by A3, FUNCT_2:def_1, RELSET_1:4;
take  g ; :: according to ALG_1:def_5 ::_thesis: g is_isomorphism U2,U1
thus  g is_isomorphism U2,U1 by A1, Th10; ::_thesis: verum
end;

theorem :: ALG_1:14
for U1, U2, U3 being Universal_Algebra st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds
U1,U3 are_isomorphic
proof
let U1, U2, U3 be Universal_Algebra; ::_thesis: ( U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic )
assume  U1,U2 are_isomorphic ; ::_thesis: ( not U2,U3 are_isomorphic or U1,U3 are_isomorphic )
then consider f being Function of U1,U2 such that
A1: f is_isomorphism U1,U2 by Def5;
assume  U2,U3 are_isomorphic ; ::_thesis: U1,U3 are_isomorphic
then consider g being Function of U2,U3 such that
A2: g is_isomorphism U2,U3 by Def5;
 g * f is_isomorphism U1,U3 by A1, A2, Th11;
hence  U1,U3 are_isomorphic by Def5; ::_thesis: verum
end;

definition
let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
assume A1: f is_homomorphism U1,U2 ;
func Image f ->  strict SubAlgebra of U2 means :Def6: :: ALG_1:def 6
 the carrier of it = f .: the carrier of U1;
existence
 ex b1 being strict SubAlgebra of U2 st the carrier of b1 = f .: the carrier of U1
proof
A2: dom f = the carrier of U1 by FUNCT_2:def_1;
then reconsider A = f .: the carrier of U1 as non empty Subset of U2 ;
take B = UniAlgSetClosed A; ::_thesis: the carrier of B = f .: the carrier of U1
 A is opers_closed
proof
let o2 be operation of U2; :: according to UNIALG_2:def_4 ::_thesis: A is_closed_on o2
consider n being Nat such that
A3: n in dom the charact of U2 and
A4: the charact of U2 . n = o2 by FINSEQ_2:10;
let s be FinSequence of A; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o2 or o2 . s in A )
assume A5: len s = arity o2 ; ::_thesis: o2 . s in A
defpred S1[ set , set ] means f . $2 = s . $1;
A6: for x being set st x in dom s holds
ex y being set st
( y in the carrier of U1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in dom s implies ex y being set st
( y in the carrier of U1 & S1[x,y] ) )
assume A7: x in dom s ; ::_thesis: ex y being set st
( y in the carrier of U1 & S1[x,y] )
then reconsider x0 = x as Element of NAT ;
 s . x0 in A by A7, FINSEQ_2:11;
then consider y being set  such that
A8: y in dom f and
 y in the carrier of U1 and
A9: f . y = s . x0 by FUNCT_1:def_6;
take  y ; ::_thesis: ( y in the carrier of U1 & S1[x,y] )
thus  ( y in the carrier of U1 & S1[x,y] ) by A8, A9; ::_thesis: verum
end;
consider s1 being Function such that
A10: ( dom s1 = dom s & rng s1 c= the carrier of U1 & ( for x being set st x in dom s holds
S1[x,s1 . x] ) ) from FUNCT_1:sch_5(A6);
 dom s1 = Seg (len s) by A10, FINSEQ_1:def_3;
then reconsider s1 = s1 as FinSequence by FINSEQ_1:def_2;
reconsider s1 = s1 as FinSequence of U1 by A10, FINSEQ_1:def_4;
reconsider s1 = s1 as Element of the carrier of U1 * by FINSEQ_1:def_11;
A11: len s1 = len s by A10, FINSEQ_3:29;
A12: dom (signature U2) = Seg (len (signature U2)) by FINSEQ_1:def_3;
A13: U1,U2 are_similar by A1, Def1;
then A14: signature U1 = signature U2 by UNIALG_2:def_1;
A15: dom (signature U1) = dom (signature U2) by A13, UNIALG_2:def_1;
A16: ( len (signature U2) = len the charact of U2 & dom the charact of U2 = Seg (len the charact of U2) ) by FINSEQ_1:def_3, UNIALG_1:def_4;
then A17: (signature U2) . n = arity o2 by A3, A4, A12, UNIALG_1:def_4;
A18: len (f * s1) = len s1 by FINSEQ_3:120;
A19: ( dom (f * s1) = Seg (len (f * s1)) & dom s = Seg (len s1) ) by A10, FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_s_holds_
(f_*_s1)_._m_=_s_._m
let m be Nat; ::_thesis: ( m in dom s implies (f * s1) . m = s . m )
assume A20: m in dom s ; ::_thesis: (f * s1) . m = s . m
then  f . (s1 . m) = s . m by A10;
hence  (f * s1) . m = s . m by A18, A19, A20, FINSEQ_3:120; ::_thesis: verum
end;
then A21: s = f * s1 by A11, A18, FINSEQ_2:9;
A22: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3;
A23: ( len (signature U1) = len the charact of U1 & dom the charact of U1 = Seg (len the charact of U1) ) by FINSEQ_1:def_3, UNIALG_1:def_4;
then reconsider o1 = the charact of U1 . n as operation of U1 by A3, A16, A22, A15, A12, FUNCT_1:def_3;
 (signature U1) . n = arity o1 by A3, A16, A15, A12, UNIALG_1:def_4;
then  s1 in  {  w where w is Element of the carrier of U1 * : len w = arity o1  }  by A14, A5, A17, A11;
then  s1 in (arity o1) -tuples_on the carrier of U1 by FINSEQ_2:def_4;
then A24: s1 in dom o1 by MARGREL1:22;
then A25: o1 . s1 in rng o1 by FUNCT_1:def_3;
 f . (o1 . s1) = o2 . (f * s1) by A1, A3, A4, A23, A16, A22, A15, A12, A24, Def1;
hence  o2 . s in A by A2, A21, A25, FUNCT_1:def_6; ::_thesis: verum
end;
then  B = UAStr(# A,(Opers (U2,A)) #) by UNIALG_2:def_8;
hence  the carrier of B = f .: the carrier of U1 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict SubAlgebra of U2 st the carrier of b1 = f .: the carrier of U1 & the carrier of b2 = f .: the carrier of U1 holds
b1 = b2
proof
let A, B be strict SubAlgebra of U2; ::_thesis: ( the carrier of A = f .: the carrier of U1 & the carrier of B = f .: the carrier of U1 implies A = B )
reconsider A1 = the carrier of A as non empty Subset of U2 by UNIALG_2:def_7;
 the charact of A = Opers (U2,A1) by UNIALG_2:def_7;
hence  ( the carrier of A = f .: the carrier of U1 & the carrier of B = f .: the carrier of U1 implies A = B ) by UNIALG_2:def_7; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Image ALG_1:def_6_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
for b4 being strict SubAlgebra of U2 holds
( b4 = Image f iff the carrier of b4 = f .: the carrier of U1 );

theorem :: ALG_1:15
for U1, U2 being Universal_Algebra
for h being Function of U1,U2 st h is_homomorphism U1,U2 holds
rng h = the carrier of (Image h)
proof
let U1, U2 be Universal_Algebra; ::_thesis: for h being Function of U1,U2 st h is_homomorphism U1,U2 holds
rng h = the carrier of (Image h)
let h be Function of U1,U2; ::_thesis: ( h is_homomorphism U1,U2 implies rng h = the carrier of (Image h) )
 dom h = the carrier of U1 by FUNCT_2:def_1;
then A1: rng h = h .: the carrier of U1 by RELAT_1:113;
assume  h is_homomorphism U1,U2 ; ::_thesis: rng h = the carrier of (Image h)
hence  rng h = the carrier of (Image h) by A1, Def6; ::_thesis: verum
end;

theorem :: ALG_1:16
for U1 being Universal_Algebra
for U2 being strict Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
( f is_epimorphism U1,U2 iff Image f = U2 )
proof
let U1 be Universal_Algebra; ::_thesis: for U2 being strict Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
( f is_epimorphism U1,U2 iff Image f = U2 )
let U2 be strict Universal_Algebra; ::_thesis: for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
( f is_epimorphism U1,U2 iff Image f = U2 )
let f be Function of U1,U2; ::_thesis: ( f is_homomorphism U1,U2 implies ( f is_epimorphism U1,U2 iff Image f = U2 ) )
assume A1: f is_homomorphism U1,U2 ; ::_thesis: ( f is_epimorphism U1,U2 iff Image f = U2 )
thus  ( f is_epimorphism U1,U2 implies Image f = U2 ) ::_thesis: ( Image f = U2 implies f is_epimorphism U1,U2 )
proof
reconsider B = the carrier of (Image f) as non empty Subset of U2 by UNIALG_2:def_7;
assume  f is_epimorphism U1,U2 ; ::_thesis: Image f = U2
then A2: the carrier of U2 = rng f by Def3
.= f .: (dom f) by RELAT_1:113
.= f .: the carrier of U1 by FUNCT_2:def_1
.= the carrier of (Image f) by A1, Def6 ;
 the charact of (Image f) = Opers (U2,B) by UNIALG_2:def_7;
hence  Image f = U2 by A2, Th1; ::_thesis: verum
end;
assume  Image f = U2 ; ::_thesis: f is_epimorphism U1,U2
then  the carrier of U2 = f .: the carrier of U1 by A1, Def6
.= f .: (dom f) by FUNCT_2:def_1
.= rng f by RELAT_1:113 ;
hence  f is_epimorphism U1,U2 by A1, Def3; ::_thesis: verum
end;

begin

definition
let U1 be 1-sorted ;
mode Relation of U1 is Relation of the carrier of U1;
mode Equivalence_Relation of U1 is Equivalence_Relation of the carrier of U1;
end;

definition
let U1 be Universal_Algebra;
mode Congruence of U1 ->  Equivalence_Relation of U1 means :Def7: :: ALG_1:def 7
 for n being Element of NAT
for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel it holds
[(o1 . x),(o1 . y)] in it;
existence
 ex b1 being Equivalence_Relation of U1 st
for n being Element of NAT
for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel b1 holds
[(o1 . x),(o1 . y)] in b1
proof
reconsider P = id the carrier of U1 as Equivalence_Relation of U1 ;
take  P ; ::_thesis: for n being Element of NAT
for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P
let n be Element of NAT ; ::_thesis: for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P
let o1 be operation of U1; ::_thesis: ( n in dom the charact of U1 & o1 = the charact of U1 . n implies for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P )
assume that
 n in dom the charact of U1 and
 o1 = the charact of U1 . n ; ::_thesis: for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P
let x, y be FinSequence of U1; ::_thesis: ( x in dom o1 & y in dom o1 & [x,y] in ExtendRel P implies [(o1 . x),(o1 . y)] in P )
assume that
A1: x in dom o1 and
 y in dom o1 and
A2: [x,y] in ExtendRel P ; ::_thesis: [(o1 . x),(o1 . y)] in P
 [x,y] in id ( the carrier of U1 *) by A2, FINSEQ_3:121;
then A3: x = y by RELAT_1:def_10;
 o1 . x in rng o1 by A1, FUNCT_1:def_3;
hence  [(o1 . x),(o1 . y)] in P by A3, RELAT_1:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Congruence ALG_1:def_7_:_
 for U1 being Universal_Algebra
for b2 being Equivalence_Relation of U1 holds
( b2 is Congruence of U1 iff for n being Element of NAT
for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel b2 holds
[(o1 . x),(o1 . y)] in b2 );

definition
let U1 be Universal_Algebra;
let E be Congruence of U1;
let o be operation of U1;
func QuotOp (o,E) ->  non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) means :Def8: :: ALG_1:def 8
( dom it = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom it holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
it . y = Class (E,(o . x)) ) );
existence
 ex b1 being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) st
( dom b1 = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b1 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b1 . y = Class (E,(o . x)) ) )
proof
defpred S1[ set , set ] means  for y being FinSequence of Class E st y = $1 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
$2 = Class (E,(o . x));
set X = (arity o) -tuples_on (Class E);
A1: for e being set st e in (arity o) -tuples_on (Class E) holds
ex u being set st
( u in Class E & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in (arity o) -tuples_on (Class E) implies ex u being set st
( u in Class E & S1[e,u] ) )
A2: dom o = (arity o) -tuples_on the carrier of U1 by MARGREL1:22
.=  {  q where q is Element of the carrier of U1 * : len q = arity o  }  by FINSEQ_2:def_4 ;
assume  e in (arity o) -tuples_on (Class E) ; ::_thesis: ex u being set st
( u in Class E & S1[e,u] )
then  e in  {  s where s is Element of (Class E) * : len s = arity o  }  by FINSEQ_2:def_4;
then consider s being Element of (Class E) *  such that
A3: s = e and
A4: len s = arity o ;
consider x being FinSequence of the carrier of U1 such that
A5: x is_representatives_FS s by FINSEQ_3:122;
take y = Class (E,(o . x)); ::_thesis: ( y in Class E & S1[e,y] )
A6: len x = arity o by A4, A5, FINSEQ_3:def_4;
 x is Element of the carrier of U1 * by FINSEQ_1:def_11;
then A7: x in dom o by A2, A6;
then A8: o . x in rng o by FUNCT_1:def_3;
hence  y in Class E by EQREL_1:def_3; ::_thesis: S1[e,y]
let a be FinSequence of Class E; ::_thesis: ( a = e implies for x being FinSequence of the carrier of U1 st x is_representatives_FS a holds
y = Class (E,(o . x)) )
assume A9: a = e ; ::_thesis: for x being FinSequence of the carrier of U1 st x is_representatives_FS a holds
y = Class (E,(o . x))
let b be FinSequence of the carrier of U1; ::_thesis: ( b is_representatives_FS a implies y = Class (E,(o . b)) )
assume A10: b is_representatives_FS a ; ::_thesis: y = Class (E,(o . b))
then A11: len b = arity o by A3, A4, A9, FINSEQ_3:def_4;
 for m being Element of NAT st m in dom x holds
[(x . m),(b . m)] in E
proof
let m be Element of NAT ; ::_thesis: ( m in dom x implies [(x . m),(b . m)] in E )
assume A12: m in dom x ; ::_thesis: [(x . m),(b . m)] in E
then A13: ( Class (E,(x . m)) = s . m & x . m in rng x ) by A5, FINSEQ_3:def_4, FUNCT_1:def_3;
dom x = Seg (arity o) by A6, FINSEQ_1:def_3
.= dom b by A11, FINSEQ_1:def_3 ;
then  Class (E,(b . m)) = s . m by A3, A9, A10, A12, FINSEQ_3:def_4;
hence  [(x . m),(b . m)] in E by A13, EQREL_1:35; ::_thesis: verum
end;
then A14: [x,b] in ExtendRel E by A6, A11, FINSEQ_3:def_3;
 b is Element of the carrier of U1 * by FINSEQ_1:def_11;
then  ( ex n being Nat st
( n in dom the charact of U1 & the charact of U1 . n = o ) & b in dom o ) by A2, A11, FINSEQ_2:10;
then  [(o . x),(o . b)] in E by A7, A14, Def7;
hence  y = Class (E,(o . b)) by A8, EQREL_1:35; ::_thesis: verum
end;
consider F being Function such that
A15: ( dom F = (arity o) -tuples_on (Class E) & rng F c= Class E & ( for e being set st e in (arity o) -tuples_on (Class E) holds
S1[e,F . e] ) ) from FUNCT_1:sch_5(A1);
 (arity o) -tuples_on (Class E) in  {  (m -tuples_on (Class E)) where m is Element of NAT : verum  }  ;
then  (arity o) -tuples_on (Class E) c= union  {  (m -tuples_on (Class E)) where m is Element of NAT : verum  }  by ZFMISC_1:74;
then  (arity o) -tuples_on (Class E) c= (Class E) * by FINSEQ_2:108;
then reconsider F = F as PartFunc of ((Class E) *),(Class E) by A15, RELSET_1:4;
A16: dom F =  {  t where t is Element of (Class E) * : len t = arity o  }  by A15, FINSEQ_2:def_4;
A17: for x, y being FinSequence of Class E st len x = len y & x in dom F holds
y in dom F
proof
let x, y be FinSequence of Class E; ::_thesis: ( len x = len y & x in dom F implies y in dom F )
assume that
A18: len x = len y and
A19: x in dom F ; ::_thesis: y in dom F
A20: y is Element of (Class E) * by FINSEQ_1:def_11;
 ex t1 being Element of (Class E) * st
( x = t1 & len t1 = arity o ) by A16, A19;
hence  y in dom F by A16, A18, A20; ::_thesis: verum
end;
A21: ex x being FinSequence st x in dom F
proof
set a = the Element of (arity o) -tuples_on (Class E);
 the Element of (arity o) -tuples_on (Class E) in (arity o) -tuples_on (Class E) ;
hence  ex x being FinSequence st x in dom F by A15; ::_thesis: verum
end;
 dom F is with_common_domain
proof
let x, y be FinSequence; :: according to MARGREL1:def_1 ::_thesis: ( not x in dom F or not y in dom F or len x = len y )
assume  ( x in dom F & y in dom F ) ; ::_thesis: len x = len y
then  ( ex t1 being Element of (Class E) * st
( x = t1 & len t1 = arity o ) & ex t2 being Element of (Class E) * st
( y = t2 & len t2 = arity o ) ) by A16;
hence  len x = len y ; ::_thesis: verum
end;
then reconsider F = F as non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) by A17, A21, MARGREL1:def_21, MARGREL1:def_22;
take  F ; ::_thesis: ( dom F = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x)) ) )
thus  dom F = (arity o) -tuples_on (Class E) by A15; ::_thesis: for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x))
let y be FinSequence of Class E; ::_thesis: ( y in dom F implies for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x)) )
assume A22: y in dom F ; ::_thesis: for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x))
let x be FinSequence of the carrier of U1; ::_thesis: ( x is_representatives_FS y implies F . y = Class (E,(o . x)) )
assume  x is_representatives_FS y ; ::_thesis: F . y = Class (E,(o . x))
hence  F . y = Class (E,(o . x)) by A15, A22; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) st dom b1 = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b1 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b1 . y = Class (E,(o . x)) ) & dom b2 = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b2 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b2 . y = Class (E,(o . x)) ) holds
b1 = b2
proof
let F, G be non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E); ::_thesis: ( dom F = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x)) ) & dom G = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom G holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
G . y = Class (E,(o . x)) ) implies F = G )
assume that
A23: dom F = (arity o) -tuples_on (Class E) and
A24: for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class (E,(o . x)) and
A25: dom G = (arity o) -tuples_on (Class E) and
A26: for y being FinSequence of Class E st y in dom G holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
G . y = Class (E,(o . x)) ; ::_thesis: F = G
 for a being set st a in dom F holds
F . a = G . a
proof
let a be set ; ::_thesis: ( a in dom F implies F . a = G . a )
assume A27: a in dom F ; ::_thesis: F . a = G . a
then reconsider b = a as FinSequence of Class E by FINSEQ_1:def_11;
consider x being FinSequence of the carrier of U1 such that
A28: x is_representatives_FS b by FINSEQ_3:122;
 F . b = Class (E,(o . x)) by A24, A27, A28;
hence  F . a = G . a by A23, A25, A26, A27, A28; ::_thesis: verum
end;
hence  F = G by A23, A25, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines QuotOp ALG_1:def_8_:_
 for U1 being Universal_Algebra
for E being Congruence of U1
for o being operation of U1
for b4 being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) holds
( b4 = QuotOp (o,E) iff ( dom b4 = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b4 holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b4 . y = Class (E,(o . x)) ) ) );

definition
let U1 be Universal_Algebra;
let E be Congruence of U1;
func QuotOpSeq (U1,E) ->  PFuncFinSequence of (Class E) means :Def9: :: ALG_1:def 9
( len it = len the charact of U1 & ( for n being Element of NAT st n in dom it holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
it . n = QuotOp (o1,E) ) );
existence
 ex b1 being PFuncFinSequence of (Class E) st
( len b1 = len the charact of U1 & ( for n being Element of NAT st n in dom b1 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b1 . n = QuotOp (o1,E) ) )
proof
defpred S1[ set , set ] means  for o being Element of Operations U1 st o = the charact of U1 . $1 holds
$2 = QuotOp (o,E);
A1: for n being Nat st n in Seg (len the charact of U1) holds
ex x being Element of PFuncs (((Class E) *),(Class E)) st S1[n,x]
proof
let n be Nat; ::_thesis: ( n in Seg (len the charact of U1) implies ex x being Element of PFuncs (((Class E) *),(Class E)) st S1[n,x] )
assume  n in Seg (len the charact of U1) ; ::_thesis: ex x being Element of PFuncs (((Class E) *),(Class E)) st S1[n,x]
then  n in dom the charact of U1 by FINSEQ_1:def_3;
then reconsider o = the charact of U1 . n as operation of U1 by FUNCT_1:def_3;
reconsider x = QuotOp (o,E) as Element of PFuncs (((Class E) *),(Class E)) by PARTFUN1:45;
take  x ; ::_thesis: S1[n,x]
thus  S1[n,x] ; ::_thesis: verum
end;
consider p being FinSequence of PFuncs (((Class E) *),(Class E)) such that
A2: ( dom p = Seg (len the charact of U1) & ( for n being Nat st n in Seg (len the charact of U1) holds
S1[n,p . n] ) ) from FINSEQ_1:sch_5(A1);
reconsider p = p as PFuncFinSequence of (Class E) ;
take  p ; ::_thesis: ( len p = len the charact of U1 & ( for n being Element of NAT st n in dom p holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E) ) )
thus  len p = len the charact of U1 by A2, FINSEQ_1:def_3; ::_thesis: for n being Element of NAT st n in dom p holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E)
let n be Element of NAT ; ::_thesis: ( n in dom p implies for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E) )
assume  n in dom p ; ::_thesis: for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E)
hence  for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PFuncFinSequence of (Class E) st len b1 = len the charact of U1 & ( for n being Element of NAT st n in dom b1 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b1 . n = QuotOp (o1,E) ) & len b2 = len the charact of U1 & ( for n being Element of NAT st n in dom b2 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b2 . n = QuotOp (o1,E) ) holds
b1 = b2
proof
let F, G be PFuncFinSequence of (Class E); ::_thesis: ( len F = len the charact of U1 & ( for n being Element of NAT st n in dom F holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
F . n = QuotOp (o1,E) ) & len G = len the charact of U1 & ( for n being Element of NAT st n in dom G holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
G . n = QuotOp (o1,E) ) implies F = G )
assume that
A3: len F = len the charact of U1 and
A4: for n being Element of NAT st n in dom F holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
F . n = QuotOp (o1,E) and
A5: len G = len the charact of U1 and
A6: for n being Element of NAT st n in dom G holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
G . n = QuotOp (o1,E) ; ::_thesis: F = G
now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_
F_._n_=_G_._n
let n be Nat; ::_thesis: ( n in dom F implies F . n = G . n )
assume A7: n in dom F ; ::_thesis: F . n = G . n
 dom F = Seg (len the charact of U1) by A3, FINSEQ_1:def_3;
then  n in dom the charact of U1 by A7, FINSEQ_1:def_3;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def_3;
A8: ( dom F = dom the charact of U1 & dom G = dom the charact of U1 ) by A3, A5, FINSEQ_3:29;
 F . n = QuotOp (o1,E) by A4, A7;
hence  F . n = G . n by A6, A8, A7; ::_thesis: verum
end;
hence  F = G by A3, A5, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines QuotOpSeq ALG_1:def_9_:_
 for U1 being Universal_Algebra
for E being Congruence of U1
for b3 being PFuncFinSequence of (Class E) holds
( b3 = QuotOpSeq (U1,E) iff ( len b3 = len the charact of U1 & ( for n being Element of NAT st n in dom b3 holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b3 . n = QuotOp (o1,E) ) ) );

definition
let U1 be Universal_Algebra;
let E be Congruence of U1;
func QuotUnivAlg (U1,E) ->  strict Universal_Algebra equals :: ALG_1:def 10
 UAStr(# (Class E),(QuotOpSeq (U1,E)) #);
coherence
 UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is strict Universal_Algebra
proof
set UU = UAStr(# (Class E),(QuotOpSeq (U1,E)) #);
 for n being Nat
for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is homogeneous
proof
let n be Nat; ::_thesis: for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is homogeneous
let h be PartFunc of ((Class E) *),(Class E); ::_thesis: ( n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n implies h is homogeneous )
assume that
A1: n in dom (QuotOpSeq (U1,E)) and
A2: h = (QuotOpSeq (U1,E)) . n ; ::_thesis: h is homogeneous
 n in Seg (len (QuotOpSeq (U1,E))) by A1, FINSEQ_1:def_3;
then  n in Seg (len the charact of U1) by Def9;
then  n in dom the charact of U1 by FINSEQ_1:def_3;
then reconsider o = the charact of U1 . n as operation of U1 by FUNCT_1:def_3;
 (QuotOpSeq (U1,E)) . n = QuotOp (o,E) by A1, Def9;
hence  h is homogeneous by A2; ::_thesis: verum
end;
then A3: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is homogeneous by MARGREL1:def_23;
 for n being Nat
for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is quasi_total
proof
let n be Nat; ::_thesis: for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is quasi_total
let h be PartFunc of ((Class E) *),(Class E); ::_thesis: ( n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n implies h is quasi_total )
assume that
A4: n in dom (QuotOpSeq (U1,E)) and
A5: h = (QuotOpSeq (U1,E)) . n ; ::_thesis: h is quasi_total
 n in Seg (len (QuotOpSeq (U1,E))) by A4, FINSEQ_1:def_3;
then  n in Seg (len the charact of U1) by Def9;
then  n in dom the charact of U1 by FINSEQ_1:def_3;
then reconsider o = the charact of U1 . n as operation of U1 by FUNCT_1:def_3;
 (QuotOpSeq (U1,E)) . n = QuotOp (o,E) by A4, Def9;
hence  h is quasi_total by A5; ::_thesis: verum
end;
then A6: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is quasi_total by MARGREL1:def_24;
 for n being set st n in dom (QuotOpSeq (U1,E)) holds
not (QuotOpSeq (U1,E)) . n is empty
proof
let n be set ; ::_thesis: ( n in dom (QuotOpSeq (U1,E)) implies not (QuotOpSeq (U1,E)) . n is empty )
assume A7: n in dom (QuotOpSeq (U1,E)) ; ::_thesis: not (QuotOpSeq (U1,E)) . n is empty
then  n in Seg (len (QuotOpSeq (U1,E))) by FINSEQ_1:def_3;
then  n in Seg (len the charact of U1) by Def9;
then A8: n in dom the charact of U1 by FINSEQ_1:def_3;
reconsider n = n as Element of NAT by A7;
reconsider o = the charact of U1 . n as operation of U1 by A8, FUNCT_1:def_3;
 (QuotOpSeq (U1,E)) . n = QuotOp (o,E) by A7, Def9;
hence  not (QuotOpSeq (U1,E)) . n is empty ; ::_thesis: verum
end;
then A9: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is non-empty by FUNCT_1:def_9;
 the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) <> {}
proof
assume A10: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) = {} ; ::_thesis: contradiction
 len the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) = len the charact of U1 by Def9;
hence  contradiction by A10; ::_thesis: verum
end;
hence  UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is strict Universal_Algebra by A3, A6, A9, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines QuotUnivAlg ALG_1:def_10_:_
 for U1 being Universal_Algebra
for E being Congruence of U1 holds QuotUnivAlg (U1,E) = UAStr(# (Class E),(QuotOpSeq (U1,E)) #);

definition
let U1 be Universal_Algebra;
let E be Congruence of U1;
func Nat_Hom (U1,E) ->  Function of U1,(QuotUnivAlg (U1,E)) means :Def11: :: ALG_1:def 11
 for u being Element of U1 holds it . u = Class (E,u);
existence
 ex b1 being Function of U1,(QuotUnivAlg (U1,E)) st
for u being Element of U1 holds b1 . u = Class (E,u)
proof
defpred S1[ Element of U1, set ] means $2 = Class (E,$1);
A1: for x being Element of U1 ex y being Element of (QuotUnivAlg (U1,E)) st S1[x,y]
proof
let x be Element of U1; ::_thesis: ex y being Element of (QuotUnivAlg (U1,E)) st S1[x,y]
reconsider y = Class (E,x) as Element of (QuotUnivAlg (U1,E)) by EQREL_1:def_3;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function of U1,(QuotUnivAlg (U1,E)) such that
A2: for x being Element of U1 holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for u being Element of U1 holds f . u = Class (E,u)
thus  for u being Element of U1 holds f . u = Class (E,u) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of U1,(QuotUnivAlg (U1,E)) st ( for u being Element of U1 holds b1 . u = Class (E,u) ) & ( for u being Element of U1 holds b2 . u = Class (E,u) ) holds
b1 = b2
proof
let f, g be Function of U1,(QuotUnivAlg (U1,E)); ::_thesis: ( ( for u being Element of U1 holds f . u = Class (E,u) ) & ( for u being Element of U1 holds g . u = Class (E,u) ) implies f = g )
assume that
A3: for u being Element of U1 holds f . u = Class (E,u) and
A4: for u being Element of U1 holds g . u = Class (E,u) ; ::_thesis: f = g
now__::_thesis:_for_u_being_Element_of_U1_holds_f_._u_=_g_._u
let u be Element of U1; ::_thesis: f . u = g . u
 f . u = Class (E,u) by A3;
hence  f . u = g . u by A4; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines Nat_Hom ALG_1:def_11_:_
 for U1 being Universal_Algebra
for E being Congruence of U1
for b3 being Function of U1,(QuotUnivAlg (U1,E)) holds
( b3 = Nat_Hom (U1,E) iff for u being Element of U1 holds b3 . u = Class (E,u) );

theorem Th17: :: ALG_1:17
for U1 being Universal_Algebra
for E being Congruence of U1 holds Nat_Hom (U1,E) is_homomorphism U1, QuotUnivAlg (U1,E)
proof
let U1 be Universal_Algebra; ::_thesis: for E being Congruence of U1 holds Nat_Hom (U1,E) is_homomorphism U1, QuotUnivAlg (U1,E)
let E be Congruence of U1; ::_thesis: Nat_Hom (U1,E) is_homomorphism U1, QuotUnivAlg (U1,E)
set f = Nat_Hom (U1,E);
set u1 = the carrier of U1;
set qu = the carrier of (QuotUnivAlg (U1,E));
A1: len (signature U1) = len the charact of U1 by UNIALG_1:def_4;
A2: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3;
A3: len (QuotOpSeq (U1,E)) = len the charact of U1 by Def9;
A4: len (signature (QuotUnivAlg (U1,E))) = len the charact of (QuotUnivAlg (U1,E)) by UNIALG_1:def_4;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_(signature_U1)_holds_
(signature_U1)_._n_=_(signature_(QuotUnivAlg_(U1,E)))_._n
let n be Nat; ::_thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature (QuotUnivAlg (U1,E))) . n )
assume A5: n in dom (signature U1) ; ::_thesis: (signature U1) . n = (signature (QuotUnivAlg (U1,E))) . n
then  n in dom the charact of U1 by A1, A2, FINSEQ_1:def_3;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def_3;
 n in dom (QuotOpSeq (U1,E)) by A3, A1, A2, A5, FINSEQ_1:def_3;
then A6: (QuotOpSeq (U1,E)) . n = QuotOp (o1,E) by Def9;
reconsider cl = QuotOp (o1,E) as non empty homogeneous quasi_total PartFunc of ( the carrier of (QuotUnivAlg (U1,E)) *), the carrier of (QuotUnivAlg (U1,E)) ;
consider b being set  such that
A7: b in dom cl by XBOOLE_0:def_1;
reconsider b = b as Element of the carrier of (QuotUnivAlg (U1,E)) * by A7;
 dom (QuotOp (o1,E)) = (arity o1) -tuples_on (Class E) by Def8;
then  b in  {  w where w is Element of (Class E) * : len w = arity o1  }  by A7, FINSEQ_2:def_4;
then  ex w being Element of (Class E) * st
( w = b & len w = arity o1 ) ;
then A8: arity cl = arity o1 by A7, MARGREL1:def_25;
 ( n in dom (signature (QuotUnivAlg (U1,E))) & (signature U1) . n = arity o1 ) by A3, A4, A2, A5, FINSEQ_1:def_3, UNIALG_1:def_4;
hence  (signature U1) . n = (signature (QuotUnivAlg (U1,E))) . n by A6, A8, UNIALG_1:def_4; ::_thesis: verum
end;
hence  signature U1 = signature (QuotUnivAlg (U1,E)) by A3, A4, A1, FINSEQ_2:9; :: according to UNIALG_2:def_1,ALG_1:def_1 ::_thesis: for n being Element of NAT st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
let n be Element of NAT ; ::_thesis: ( n in dom the charact of U1 implies for o1 being operation of U1
for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) )
assume  n in dom the charact of U1 ; ::_thesis: for o1 being operation of U1
for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
then  n in Seg (len the charact of U1) by FINSEQ_1:def_3;
then A9: n in dom (QuotOpSeq (U1,E)) by A3, FINSEQ_1:def_3;
let o1 be operation of U1; ::_thesis: for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
let o2 be operation of (QuotUnivAlg (U1,E)); ::_thesis: ( o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n implies for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) )
assume  ( the charact of U1 . n = o1 & o2 = the charact of (QuotUnivAlg (U1,E)) . n ) ; ::_thesis: for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
then A10: o2 = QuotOp (o1,E) by A9, Def9;
let x be FinSequence of U1; ::_thesis: ( x in dom o1 implies (Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) )
reconsider x1 = x as Element of the carrier of U1 * by FINSEQ_1:def_11;
reconsider fx = (Nat_Hom (U1,E)) * x as FinSequence of Class E ;
reconsider fx = fx as Element of (Class E) * by FINSEQ_1:def_11;
A11: len ((Nat_Hom (U1,E)) * x) = len x by FINSEQ_3:120;
now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_x_holds_
Class_(E,(x_._m))_=_fx_._m
let m be Element of NAT ; ::_thesis: ( m in dom x implies Class (E,(x . m)) = fx . m )
assume A12: m in dom x ; ::_thesis: Class (E,(x . m)) = fx . m
then A13: m in dom ((Nat_Hom (U1,E)) * x) by FINSEQ_3:120;
 x . m in rng x by A12, FUNCT_1:def_3;
then reconsider xm = x . m as Element of the carrier of U1 ;
thus  Class (E,(x . m)) = (Nat_Hom (U1,E)) . xm by Def11
.= fx . m by A13, FINSEQ_3:120 ; ::_thesis: verum
end;
then A14: x is_representatives_FS fx by A11, FINSEQ_3:def_4;
assume A15: x in dom o1 ; ::_thesis: (Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
then  o1 . x in rng o1 by FUNCT_1:def_3;
then reconsider ox = o1 . x as Element of the carrier of U1 ;
dom o1 = (arity o1) -tuples_on the carrier of U1 by MARGREL1:22
.=  {  p where p is Element of the carrier of U1 * : len p = arity o1  }  by FINSEQ_2:def_4 ;
then A16: ex p being Element of the carrier of U1 * st
( p = x1 & len p = arity o1 ) by A15;
A17: (Nat_Hom (U1,E)) . (o1 . x) = Class (E,ox) by Def11
.= Class (E,(o1 . x)) ;
dom (QuotOp (o1,E)) = (arity o1) -tuples_on (Class E) by Def8
.=  {  q where q is Element of (Class E) * : len q = arity o1  }  by FINSEQ_2:def_4 ;
then  fx in dom (QuotOp (o1,E)) by A16, A11;
hence  (Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) by A17, A10, A14, Def8; ::_thesis: verum
end;

theorem :: ALG_1:18
for U1 being Universal_Algebra
for E being Congruence of U1 holds Nat_Hom (U1,E) is_epimorphism U1, QuotUnivAlg (U1,E)
proof
let U1 be Universal_Algebra; ::_thesis: for E being Congruence of U1 holds Nat_Hom (U1,E) is_epimorphism U1, QuotUnivAlg (U1,E)
let E be Congruence of U1; ::_thesis: Nat_Hom (U1,E) is_epimorphism U1, QuotUnivAlg (U1,E)
set f = Nat_Hom (U1,E);
set qa = QuotUnivAlg (U1,E);
set cqa = the carrier of (QuotUnivAlg (U1,E));
set u1 = the carrier of U1;
thus  Nat_Hom (U1,E) is_homomorphism U1, QuotUnivAlg (U1,E) by Th17; :: according to ALG_1:def_3 ::_thesis: rng (Nat_Hom (U1,E)) = the carrier of (QuotUnivAlg (U1,E))
thus  rng (Nat_Hom (U1,E)) c= the carrier of (QuotUnivAlg (U1,E)) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (QuotUnivAlg (U1,E)) c= rng (Nat_Hom (U1,E))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (QuotUnivAlg (U1,E)) or x in rng (Nat_Hom (U1,E)) )
assume A1: x in the carrier of (QuotUnivAlg (U1,E)) ; ::_thesis: x in rng (Nat_Hom (U1,E))
then reconsider x1 = x as Subset of the carrier of U1 ;
consider y being set  such that
A2: y in the carrier of U1 and
A3: x1 = Class (E,y) by A1, EQREL_1:def_3;
reconsider y = y as Element of the carrier of U1 by A2;
 dom (Nat_Hom (U1,E)) = the carrier of U1 by FUNCT_2:def_1;
then  (Nat_Hom (U1,E)) . y in rng (Nat_Hom (U1,E)) by FUNCT_1:def_3;
hence  x in rng (Nat_Hom (U1,E)) by A3, Def11; ::_thesis: verum
end;

definition
let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
assume A1: f is_homomorphism U1,U2 ;
func Cng f ->  Congruence of U1 means :Def12: :: ALG_1:def 12
 for a, b being Element of U1 holds
( [a,b] in it iff f . a = f . b );
existence
 ex b1 being Congruence of U1 st
for a, b being Element of U1 holds
( [a,b] in b1 iff f . a = f . b )
proof
defpred S1[ set , set ] means f . $1 = f . $2;
set u1 = the carrier of U1;
consider R being Relation of the carrier of U1, the carrier of U1 such that
A2: for x, y being Element of the carrier of U1 holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
 R is_reflexive_in the carrier of U1
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of U1 or [x,x] in R )
assume  x in the carrier of U1 ; ::_thesis: [x,x] in R
then reconsider x1 = x as Element of the carrier of U1 ;
 f . x1 = f . x1 ;
hence  [x,x] in R by A2; ::_thesis: verum
end;
then A3: ( dom R = the carrier of U1 & field R = the carrier of U1 ) by ORDERS_1:13;
A4: R is_transitive_in the carrier of U1
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of U1 or not y in the carrier of U1 or not z in the carrier of U1 or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A5: ( x in the carrier of U1 & y in the carrier of U1 & z in the carrier of U1 ) and
A6: ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R
reconsider x1 = x, y1 = y, z1 = z as Element of the carrier of U1 by A5;
 ( f . x1 = f . y1 & f . y1 = f . z1 ) by A2, A6;
hence  [x,z] in R by A2; ::_thesis: verum
end;
 R is_symmetric_in the carrier of U1
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in the carrier of U1 or not b1 in the carrier of U1 or not [x,b1] in R or [b1,x] in R )
let y be set ; ::_thesis: ( not x in the carrier of U1 or not y in the carrier of U1 or not [x,y] in R or [y,x] in R )
assume that
A7: ( x in the carrier of U1 & y in the carrier of U1 ) and
A8: [x,y] in R ; ::_thesis: [y,x] in R
reconsider x1 = x, y1 = y as Element of the carrier of U1 by A7;
 f . x1 = f . y1 by A2, A8;
hence  [y,x] in R by A2; ::_thesis: verum
end;
then reconsider R = R as Equivalence_Relation of U1 by A3, A4, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
now__::_thesis:_for_n_being_Element_of_NAT_
for_o_being_operation_of_U1_st_n_in_dom_the_charact_of_U1_&_o_=_the_charact_of_U1_._n_holds_
for_x,_y_being_FinSequence_of_U1_st_x_in_dom_o_&_y_in_dom_o_&_[x,y]_in_ExtendRel_R_holds_
[(o_._x),(o_._y)]_in_R
 U1,U2 are_similar by A1, Def1;
then A9: signature U1 = signature U2 by UNIALG_2:def_1;
let n be Element of NAT ; ::_thesis: for o being operation of U1 st n in dom the charact of U1 & o = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R
let o be operation of U1; ::_thesis: ( n in dom the charact of U1 & o = the charact of U1 . n implies for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R )
assume that
A10: n in dom the charact of U1 and
A11: o = the charact of U1 . n ; ::_thesis: for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R
 ( len (signature U1) = len the charact of U1 & len (signature U2) = len the charact of U2 ) by UNIALG_1:def_4;
then  dom the charact of U2 = dom the charact of U1 by A9, FINSEQ_3:29;
then reconsider o2 = the charact of U2 . n as operation of U2 by A10, FUNCT_1:def_3;
let x, y be FinSequence of U1; ::_thesis: ( x in dom o & y in dom o & [x,y] in ExtendRel R implies [(o . x),(o . y)] in R )
assume that
A12: ( x in dom o & y in dom o ) and
A13: [x,y] in ExtendRel R ; ::_thesis: [(o . x),(o . y)] in R
 ( o . x in rng o & o . y in rng o ) by A12, FUNCT_1:def_3;
then reconsider ox = o . x, oy = o . y as Element of the carrier of U1 ;
A14: len x = len y by A13, FINSEQ_3:def_3;
A15: len (f * y) = len y by FINSEQ_3:120;
then A16: dom (f * y) = Seg (len x) by A14, FINSEQ_1:def_3;
A17: len (f * x) = len x by FINSEQ_3:120;
A18: now__::_thesis:_for_m_being_Nat_st_m_in_dom_(f_*_y)_holds_
(f_*_y)_._m_=_(f_*_x)_._m
let m be Nat; ::_thesis: ( m in dom (f * y) implies (f * y) . m = (f * x) . m )
assume A19: m in dom (f * y) ; ::_thesis: (f * y) . m = (f * x) . m
then  m in dom y by A14, A16, FINSEQ_1:def_3;
then A20: y . m in rng y by FUNCT_1:def_3;
A21: m in dom x by A16, A19, FINSEQ_1:def_3;
then  x . m in rng x by FUNCT_1:def_3;
then reconsider xm = x . m, ym = y . m as Element of the carrier of U1 by A20;
 [(x . m),(y . m)] in R by A13, A21, FINSEQ_3:def_3;
then A22: f . xm = f . ym by A2
.= (f * y) . m by A19, FINSEQ_3:120 ;
 m in dom (f * x) by A17, A16, A19, FINSEQ_1:def_3;
hence  (f * y) . m = (f * x) . m by A22, FINSEQ_3:120; ::_thesis: verum
end;
 ( f . (o . x) = o2 . (f * x) & f . (o . y) = o2 . (f * y) ) by A1, A10, A11, A12, Def1;
then  f . ox = f . oy by A14, A17, A15, A18, FINSEQ_2:9;
hence  [(o . x),(o . y)] in R by A2; ::_thesis: verum
end;
then reconsider R = R as Congruence of U1 by Def7;
take  R ; ::_thesis: for a, b being Element of U1 holds
( [a,b] in R iff f . a = f . b )
let a, b be Element of the carrier of U1; ::_thesis: ( [a,b] in R iff f . a = f . b )
thus  ( [a,b] in R implies f . a = f . b ) by A2; ::_thesis: ( f . a = f . b implies [a,b] in R )
assume  f . a = f . b ; ::_thesis: [a,b] in R
hence  [a,b] in R by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Congruence of U1 st ( for a, b being Element of U1 holds
( [a,b] in b1 iff f . a = f . b ) ) & ( for a, b being Element of U1 holds
( [a,b] in b2 iff f . a = f . b ) ) holds
b1 = b2
proof
set u1 = the carrier of U1;
let X, Y be Congruence of U1; ::_thesis: ( ( for a, b being Element of U1 holds
( [a,b] in X iff f . a = f . b ) ) & ( for a, b being Element of U1 holds
( [a,b] in Y iff f . a = f . b ) ) implies X = Y )
assume that
A23: for a, b being Element of U1 holds
( [a,b] in X iff f . a = f . b ) and
A24: for a, b being Element of U1 holds
( [a,b] in Y iff f . a = f . b ) ; ::_thesis: X = Y
 for x, y being set holds
( [x,y] in X iff [x,y] in Y )
proof
let x, y be set ; ::_thesis: ( [x,y] in X iff [x,y] in Y )
thus  ( [x,y] in X implies [x,y] in Y ) ::_thesis: ( [x,y] in Y implies [x,y] in X )
proof
assume A25: [x,y] in X ; ::_thesis: [x,y] in Y
then reconsider x1 = x, y1 = y as Element of the carrier of U1 by ZFMISC_1:87;
 f . x1 = f . y1 by A23, A25;
hence  [x,y] in Y by A24; ::_thesis: verum
end;
assume A26: [x,y] in Y ; ::_thesis: [x,y] in X
then reconsider x1 = x, y1 = y as Element of the carrier of U1 by ZFMISC_1:87;
 f . x1 = f . y1 by A24, A26;
hence  [x,y] in X by A23; ::_thesis: verum
end;
hence  X = Y by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines Cng ALG_1:def_12_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
for b4 being Congruence of U1 holds
( b4 = Cng f iff for a, b being Element of U1 holds
( [a,b] in b4 iff f . a = f . b ) );

definition
let U1, U2 be Universal_Algebra;
let f be Function of U1,U2;
assume A1: f is_homomorphism U1,U2 ;
func HomQuot f ->  Function of (QuotUnivAlg (U1,(Cng f))),U2 means :Def13: :: ALG_1:def 13
 for a being Element of U1 holds it . (Class ((Cng f),a)) = f . a;
existence
 ex b1 being Function of (QuotUnivAlg (U1,(Cng f))),U2 st
for a being Element of U1 holds b1 . (Class ((Cng f),a)) = f . a
proof
set qa = QuotUnivAlg (U1,(Cng f));
set cqa = the carrier of (QuotUnivAlg (U1,(Cng f)));
set u1 = the carrier of U1;
set u2 = the carrier of U2;
defpred S1[ set , set ] means  for a being Element of the carrier of U1 st $1 = Class ((Cng f),a) holds
$2 = f . a;
A2: for x being set st x in the carrier of (QuotUnivAlg (U1,(Cng f))) holds
ex y being set st
( y in the carrier of U2 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of (QuotUnivAlg (U1,(Cng f))) implies ex y being set st
( y in the carrier of U2 & S1[x,y] ) )
assume A3: x in the carrier of (QuotUnivAlg (U1,(Cng f))) ; ::_thesis: ex y being set st
( y in the carrier of U2 & S1[x,y] )
then reconsider x1 = x as Subset of the carrier of U1 ;
consider a being set  such that
A4: a in the carrier of U1 and
A5: x1 = Class ((Cng f),a) by A3, EQREL_1:def_3;
reconsider a = a as Element of the carrier of U1 by A4;
take y = f . a; ::_thesis: ( y in the carrier of U2 & S1[x,y] )
thus  y in the carrier of U2 ; ::_thesis: S1[x,y]
let b be Element of the carrier of U1; ::_thesis: ( x = Class ((Cng f),b) implies y = f . b )
assume  x = Class ((Cng f),b) ; ::_thesis: y = f . b
then  b in Class ((Cng f),a) by A5, EQREL_1:23;
then  [b,a] in Cng f by EQREL_1:19;
hence  y = f . b by A1, Def12; ::_thesis: verum
end;
consider F being Function such that
A6: ( dom F = the carrier of (QuotUnivAlg (U1,(Cng f))) & rng F c= the carrier of U2 & ( for x being set st x in the carrier of (QuotUnivAlg (U1,(Cng f))) holds
S1[x,F . x] ) ) from FUNCT_1:sch_5(A2);
reconsider F = F as Function of (QuotUnivAlg (U1,(Cng f))),U2 by A6, FUNCT_2:def_1, RELSET_1:4;
take  F ; ::_thesis: for a being Element of U1 holds F . (Class ((Cng f),a)) = f . a
let a be Element of the carrier of U1; ::_thesis: F . (Class ((Cng f),a)) = f . a
 Class ((Cng f),a) in Class (Cng f) by EQREL_1:def_3;
hence  F . (Class ((Cng f),a)) = f . a by A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (QuotUnivAlg (U1,(Cng f))),U2 st ( for a being Element of U1 holds b1 . (Class ((Cng f),a)) = f . a ) & ( for a being Element of U1 holds b2 . (Class ((Cng f),a)) = f . a ) holds
b1 = b2
proof
set qa = QuotUnivAlg (U1,(Cng f));
set cqa = the carrier of (QuotUnivAlg (U1,(Cng f)));
set u1 = the carrier of U1;
let F, G be Function of (QuotUnivAlg (U1,(Cng f))),U2; ::_thesis: ( ( for a being Element of U1 holds F . (Class ((Cng f),a)) = f . a ) & ( for a being Element of U1 holds G . (Class ((Cng f),a)) = f . a ) implies F = G )
assume that
A7: for a being Element of the carrier of U1 holds F . (Class ((Cng f),a)) = f . a and
A8: for a being Element of the carrier of U1 holds G . (Class ((Cng f),a)) = f . a ; ::_thesis: F = G
let x be Element of the carrier of (QuotUnivAlg (U1,(Cng f))); :: according to FUNCT_2:def_8 ::_thesis: F . x = G . x
 x in the carrier of (QuotUnivAlg (U1,(Cng f))) ;
then reconsider x1 = x as Subset of the carrier of U1 ;
consider a being set  such that
A9: ( a in the carrier of U1 & x1 = Class ((Cng f),a) ) by EQREL_1:def_3;
thus F . x = f . a by A7, A9
.= G . x by A8, A9 ; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines HomQuot ALG_1:def_13_:_
 for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
for b4 being Function of (QuotUnivAlg (U1,(Cng f))),U2 holds
( b4 = HomQuot f iff for a being Element of U1 holds b4 . (Class ((Cng f),a)) = f . a );

theorem Th19: :: ALG_1:19
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
( HomQuot f is_homomorphism QuotUnivAlg (U1,(Cng f)),U2 & HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2 )
proof
let U1, U2 be Universal_Algebra; ::_thesis: for f being Function of U1,U2 st f is_homomorphism U1,U2 holds
( HomQuot f is_homomorphism QuotUnivAlg (U1,(Cng f)),U2 & HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2 )
let f be Function of U1,U2; ::_thesis: ( f is_homomorphism U1,U2 implies ( HomQuot f is_homomorphism QuotUnivAlg (U1,(Cng f)),U2 & HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2 ) )
set qa = QuotUnivAlg (U1,(Cng f));
set cqa = the carrier of (QuotUnivAlg (U1,(Cng f)));
set u1 = the carrier of U1;
set F = HomQuot f;
assume A1: f is_homomorphism U1,U2 ; ::_thesis: ( HomQuot f is_homomorphism QuotUnivAlg (U1,(Cng f)),U2 & HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2 )
thus A2: HomQuot f is_homomorphism QuotUnivAlg (U1,(Cng f)),U2 ::_thesis: HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2
proof
 Nat_Hom (U1,(Cng f)) is_homomorphism U1, QuotUnivAlg (U1,(Cng f)) by Th17;
then  U1, QuotUnivAlg (U1,(Cng f)) are_similar by Def1;
then A3: signature U1 = signature (QuotUnivAlg (U1,(Cng f))) by UNIALG_2:def_1;
 U1,U2 are_similar by A1, Def1;
then  signature U2 = signature (QuotUnivAlg (U1,(Cng f))) by A3, UNIALG_2:def_1;
hence  QuotUnivAlg (U1,(Cng f)),U2 are_similar by UNIALG_2:def_1; :: according to ALG_1:def_1 ::_thesis: for n being Element of NAT st n in dom the charact of (QuotUnivAlg (U1,(Cng f))) holds
for o1 being operation of (QuotUnivAlg (U1,(Cng f)))
for o2 being operation of U2 st o1 = the charact of (QuotUnivAlg (U1,(Cng f))) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg (U1,(Cng f))) st x in dom o1 holds
(HomQuot f) . (o1 . x) = o2 . ((HomQuot f) * x)
let n be Element of NAT ; ::_thesis: ( n in dom the charact of (QuotUnivAlg (U1,(Cng f))) implies for o1 being operation of (QuotUnivAlg (U1,(Cng f)))
for o2 being operation of U2 st o1 = the charact of (QuotUnivAlg (U1,(Cng f))) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg (U1,(Cng f))) st x in dom o1 holds
(HomQuot f) . (o1 . x) = o2 . ((HomQuot f) * x) )
assume A4: n in dom the charact of (QuotUnivAlg (U1,(Cng f))) ; ::_thesis: for o1 being operation of (QuotUnivAlg (U1,(Cng f)))
for o2 being operation of U2 st o1 = the charact of (QuotUnivAlg (U1,(Cng f))) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg (U1,(Cng f))) st x in dom o1 holds
(HomQuot f) . (o1 . x) = o2 . ((HomQuot f) * x)
A5: ( len (signature U1) = len the charact of U1 & len (signature (QuotUnivAlg (U1,(Cng f)))) = len the charact of (QuotUnivAlg (U1,(Cng f))) ) by UNIALG_1:def_4;
A6: ( dom the charact of (QuotUnivAlg (U1,(Cng f))) = Seg (len the charact of (QuotUnivAlg (U1,(Cng f)))) & dom the charact of U1 = Seg (len the charact of U1) ) by FINSEQ_1:def_3;
then reconsider o1 = the charact of U1 . n as operation of U1 by A3, A4, A5, FUNCT_1:def_3;
A7: dom o1 = (arity o1) -tuples_on the carrier of U1 by MARGREL1:22
.=  {  p where p is Element of the carrier of U1 * : len p = arity o1  }  by FINSEQ_2:def_4 ;
let oq be operation of (QuotUnivAlg (U1,(Cng f))); ::_thesis: for o2 being operation of U2 st oq = the charact of (QuotUnivAlg (U1,(Cng f))) . n & o2 = the charact of U2 . n holds
for x being FinSequence of (QuotUnivAlg (U1,(Cng f))) st x in dom oq holds
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)
let o2 be operation of U2; ::_thesis: ( oq = the charact of (QuotUnivAlg (U1,(Cng f))) . n & o2 = the charact of U2 . n implies for x being FinSequence of (QuotUnivAlg (U1,(Cng f))) st x in dom oq holds
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x) )
assume that
A8: oq = the charact of (QuotUnivAlg (U1,(Cng f))) . n and
A9: o2 = the charact of U2 . n ; ::_thesis: for x being FinSequence of (QuotUnivAlg (U1,(Cng f))) st x in dom oq holds
(HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)
let x be FinSequence of (QuotUnivAlg (U1,(Cng f))); ::_thesis: ( x in dom oq implies (HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x) )
assume A10: x in dom oq ; ::_thesis: (HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x)
reconsider x1 = x as FinSequence of Class (Cng f) ;
reconsider x1 = x1 as Element of (Class (Cng f)) * by FINSEQ_1:def_11;
consider y being FinSequence of U1 such that
A11: y is_representatives_FS x1 by FINSEQ_3:122;
reconsider y = y as Element of the carrier of U1 * by FINSEQ_1:def_11;
A12: len x1 = len y by A11, FINSEQ_3:def_4;
then A13: len ((HomQuot f) * x) = len y by FINSEQ_3:120;
A14: len y = len (f * y) by FINSEQ_3:120;
A15: now__::_thesis:_for_m_being_Nat_st_m_in_Seg_(len_y)_holds_
((HomQuot_f)_*_x)_._m_=_(f_*_y)_._m
let m be Nat; ::_thesis: ( m in Seg (len y) implies ((HomQuot f) * x) . m = (f * y) . m )
assume A16: m in Seg (len y) ; ::_thesis: ((HomQuot f) * x) . m = (f * y) . m
then A17: m in dom ((HomQuot f) * x) by A13, FINSEQ_1:def_3;
A18: m in dom (f * y) by A14, A16, FINSEQ_1:def_3;
A19: m in dom y by A16, FINSEQ_1:def_3;
then reconsider ym = y . m as Element of the carrier of U1 by FINSEQ_2:11;
 x1 . m = Class ((Cng f),(y . m)) by A11, A19, FINSEQ_3:def_4;
hence ((HomQuot f) * x) . m = (HomQuot f) . (Class ((Cng f),ym)) by A17, FINSEQ_3:120
.= f . (y . m) by A1, Def13
.= (f * y) . m by A18, FINSEQ_3:120 ;
::_thesis: verum
end;
 dom ((HomQuot f) * x) = Seg (len y) by A13, FINSEQ_1:def_3;
then A20: o2 . ((HomQuot f) * x) = o2 . (f * y) by A13, A14, A15, FINSEQ_2:9;
A21: oq = QuotOp (o1,(Cng f)) by A4, A8, Def9;
then  dom oq = (arity o1) -tuples_on (Class (Cng f)) by Def8
.=  {  w where w is Element of (Class (Cng f)) * : len w = arity o1  }  by FINSEQ_2:def_4 ;
then  ex w being Element of (Class (Cng f)) * st
( w = x1 & len w = arity o1 ) by A10;
then A22: y in dom o1 by A12, A7;
then  o1 . y in rng o1 by FUNCT_1:def_3;
then reconsider o1y = o1 . y as Element of the carrier of U1 ;
(HomQuot f) . (oq . x) = (HomQuot f) . (Class ((Cng f),o1y)) by A10, A11, A21, Def8
.= f . (o1 . y) by A1, Def13 ;
hence  (HomQuot f) . (oq . x) = o2 . ((HomQuot f) * x) by A1, A3, A4, A9, A6, A5, A22, A20, Def1; ::_thesis: verum
end;
A23: dom (HomQuot f) = the carrier of (QuotUnivAlg (U1,(Cng f))) by FUNCT_2:def_1;
 HomQuot f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom (HomQuot f) or not b1 in dom (HomQuot f) or not (HomQuot f) . x = (HomQuot f) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom (HomQuot f) or not y in dom (HomQuot f) or not (HomQuot f) . x = (HomQuot f) . y or x = y )
assume that
A24: x in dom (HomQuot f) and
A25: y in dom (HomQuot f) and
A26: (HomQuot f) . x = (HomQuot f) . y ; ::_thesis: x = y
reconsider x1 = x, y1 = y as Subset of the carrier of U1 by A23, A24, A25;
consider a being set  such that
A27: a in the carrier of U1 and
A28: x1 = Class ((Cng f),a) by A24, EQREL_1:def_3;
reconsider a = a as Element of the carrier of U1 by A27;
consider b being set  such that
A29: b in the carrier of U1 and
A30: y1 = Class ((Cng f),b) by A25, EQREL_1:def_3;
reconsider b = b as Element of the carrier of U1 by A29;
A31: (HomQuot f) . y1 = f . b by A1, A30, Def13;
 (HomQuot f) . x1 = f . a by A1, A28, Def13;
then  [a,b] in Cng f by A1, A26, A31, Def12;
hence  x = y by A28, A30, EQREL_1:35; ::_thesis: verum
end;
hence  HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2 by A2, Def2; ::_thesis: verum
end;

theorem Th20: :: ALG_1:20
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_epimorphism U1,U2 holds
HomQuot f is_isomorphism QuotUnivAlg (U1,(Cng f)),U2
proof
let U1, U2 be Universal_Algebra; ::_thesis: for f being Function of U1,U2 st f is_epimorphism U1,U2 holds
HomQuot f is_isomorphism QuotUnivAlg (U1,(Cng f)),U2
let f be Function of U1,U2; ::_thesis: ( f is_epimorphism U1,U2 implies HomQuot f is_isomorphism QuotUnivAlg (U1,(Cng f)),U2 )
set qa = QuotUnivAlg (U1,(Cng f));
set u1 = the carrier of U1;
set u2 = the carrier of U2;
set F = HomQuot f;
assume A1: f is_epimorphism U1,U2 ; ::_thesis: HomQuot f is_isomorphism QuotUnivAlg (U1,(Cng f)),U2
then A2: f is_homomorphism U1,U2 by Def3;
then  HomQuot f is_monomorphism QuotUnivAlg (U1,(Cng f)),U2 by Th19;
then A3: HomQuot f is one-to-one by Def2;
A4: rng f = the carrier of U2 by A1, Def3;
A5: rng (HomQuot f) = the carrier of U2
proof
thus  rng (HomQuot f) c= the carrier of U2 ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of U2 c= rng (HomQuot f)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of U2 or x in rng (HomQuot f) )
assume  x in the carrier of U2 ; ::_thesis: x in rng (HomQuot f)
then consider y being set  such that
A6: y in dom f and
A7: f . y = x by A4, FUNCT_1:def_3;
reconsider y = y as Element of the carrier of U1 by A6;
set u = Class ((Cng f),y);
A8: ( dom (HomQuot f) = the carrier of (QuotUnivAlg (U1,(Cng f))) & Class ((Cng f),y) in Class (Cng f) ) by EQREL_1:def_3, FUNCT_2:def_1;
 (HomQuot f) . (Class ((Cng f),y)) = x by A2, A7, Def13;
hence  x in rng (HomQuot f) by A8, FUNCT_1:def_3; ::_thesis: verum
end;
 HomQuot f is_homomorphism QuotUnivAlg (U1,(Cng f)),U2 by A2, Th19;
hence  HomQuot f is_isomorphism QuotUnivAlg (U1,(Cng f)),U2 by A3, A5, Th7; ::_thesis: verum
end;

theorem :: ALG_1:21
for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_epimorphism U1,U2 holds
QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic
proof
let U1, U2 be Universal_Algebra; ::_thesis: for f being Function of U1,U2 st f is_epimorphism U1,U2 holds
QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic
let f be Function of U1,U2; ::_thesis: ( f is_epimorphism U1,U2 implies QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic )
assume A1: f is_epimorphism U1,U2 ; ::_thesis: QuotUnivAlg (U1,(Cng f)),U2 are_isomorphic
take  HomQuot f ; :: according to ALG_1:def_5 ::_thesis: HomQuot f is_isomorphism QuotUnivAlg (U1,(Cng f)),U2
thus  HomQuot f is_isomorphism QuotUnivAlg (U1,(Cng f)),U2 by A1, Th20; ::_thesis: verum
end;