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