alg_1.miz



    begin

    reserve U1,U2,U3 for Universal_Algebra,

n,m for Nat,

o1 for operation of U1,

o2 for operation of U2,

o3 for operation of U3,

x,y for set;

    theorem :: ALG_1:1

    

     Th1: for B be non empty Subset of U1 st B = the carrier of U1 holds ( Opers (U1,B)) = the charact of U1

    proof

      let B be non empty Subset of U1;

      

       A1: ( dom ( Opers (U1,B))) = ( dom the charact of U1) by UNIALG_2:def 6;

      assume

       A2: B = the carrier of U1;

      now

        let n be Nat;

        assume

         A3: n in ( dom the charact of U1);

        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;

      end;

      hence thesis by A1;

    end;

    reserve a for FinSequence of U1,

f for Function of U1, U2;

    theorem :: ALG_1:2

    (f * ( <*> the carrier of U1)) = ( <*> the carrier of U2);

    theorem :: ALG_1:3

    

     Th3: (( id the carrier of U1) * a) = a

    proof

      set f = ( id the carrier of U1);

      

       A1: ( dom (f * a)) = ( dom a) by FINSEQ_3: 120;

       A2:

      now

        let n be Nat;

        assume

         A3: n in ( dom (f * a));

        then

        reconsider u = (a . n) as Element of U1 by A1, FINSEQ_2: 11;

        (f . u) = u;

        hence ((f * a) . n) = (a . n) by A3, FINSEQ_3: 120;

      end;

      ( len (f * a)) = ( len a) by FINSEQ_3: 120;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: ALG_1:4

    

     Th4: for h1 be Function of U1, U2, h2 be Function of U2, U3, a be FinSequence of U1 holds (h2 * (h1 * a)) = ((h2 * h1) * a)

    proof

      let h1 be Function of U1, U2, h2 be Function of U2, U3, a be FinSequence of U1;

      

       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) qua Function of the carrier of U1, the carrier of U3 * a qua FinSequence of the carrier of U1)) by FINSEQ_3: 120;

      then

       A5: ( dom ((h2 * h1) * a)) = ( Seg ( len a)) by FINSEQ_1:def 3;

       A6:

      now

        let n be Nat;

        assume

         A7: n in ( dom (h2 * (h1 * a)));

        

        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;

      end;

      ( len (h2 * (h1 * a))) = ( len (h1 * a)) & ( len (h1 * a)) = ( len a) by FINSEQ_3: 120;

      hence thesis by A4, A6, FINSEQ_2: 9;

    end;

    definition

      let U1, U2, f;

      :: ALG_1:def1

      pred f is_homomorphism means (U1,U2) are_similar & for n st n in ( dom the charact of U1) holds for o1, o2 st o1 = (the charact of U1 . n) & o2 = (the charact of U2 . n) holds for x be FinSequence of U1 st x in ( dom o1) holds (f . (o1 . x)) = (o2 . (f * x));

    end

    definition

      let U1, U2, f;

      :: ALG_1:def2

      pred f is_monomorphism means f is_homomorphism & f is one-to-one;

      :: ALG_1:def3

      pred f is_epimorphism means f is_homomorphism & ( rng f) = the carrier of U2;

    end

    definition

      let U1, U2, f;

      :: ALG_1:def4

      pred f is_isomorphism means f is_monomorphism & f is_epimorphism ;

    end

    definition

      let U1, U2;

      :: ALG_1:def5

      pred U1,U2 are_isomorphic means ex f st f is_isomorphism ;

    end

    theorem :: ALG_1:5

    

     Th5: ( id the carrier of U1) is_homomorphism

    proof

      thus (U1,U1) are_similar ;

      let n;

      assume n in ( dom the charact of U1);

      let o1,o2 be operation of U1;

      assume

       A1: o1 = (the charact of U1 . n) & o2 = (the charact of U1 . n);

      set f = ( id the carrier of U1);

      let x be FinSequence of U1;

      assume x in ( dom o1);

      then (o1 . x) in ( rng o1) by FUNCT_1:def 3;

      then

      reconsider u = (o1 . x) as Element of U1;

      (f . u) = u;

      hence thesis by A1, Th3;

    end;

    theorem :: ALG_1:6

    

     Th6: for h1 be Function of U1, U2, h2 be Function of U2, U3 st h1 is_homomorphism & h2 is_homomorphism holds (h2 * h1) is_homomorphism

    proof

      let h1 be Function of U1, U2, h2 be Function of U2, U3;

      set s1 = ( signature U1), s2 = ( signature U2), s3 = ( signature U3);

      assume that

       A1: h1 is_homomorphism and

       A2: h2 is_homomorphism ;

      (U1,U2) are_similar by A1;

      then

       A3: s1 = s2;

      (U2,U3) are_similar by A2;

      hence s1 = s3 by A3;

      let n;

      assume

       A4: n in ( dom the charact of U1);

      let o1, o3;

      assume that

       A5: o1 = (the charact of U1 . n) and

       A6: o3 = (the charact of U3 . n);

      let a;

      reconsider b = (h1 * a) as Element of (the carrier of U2 * ) by FINSEQ_1:def 11;

      assume

       A7: a in ( dom o1);

      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 be Element of (the carrier of U1 * ) : ( len w) = ( arity o1) } by A7, FINSEQ_2:def 4;

      then

       A9: ex w be Element of (the carrier of U1 * ) st w = a & ( len w) = ( arity o1);

      

       A10: ( len s1) = ( 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 s2) = ( 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 s1) = ( Seg ( len s1)) by FINSEQ_1:def 3;

      then

       A13: (s2 . n) = ( arity o2) by A3, A10, A4, UNIALG_1:def 4;

      (s1 . 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 be 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;

      (h1 . (o1 . a)) = (o2 . (h1 * a)) by A1, A4, A5, A7;

      

      hence ((h2 * h1) . (o1 . a)) = (o3 . (h2 * (h1 * a))) by A8, A14, FUNCT_2: 15

      .= (o3 . ((h2 * h1) * a)) by Th4;

    end;

    theorem :: ALG_1:7

    

     Th7: f is_isomorphism iff f is_homomorphism & ( rng f) = the carrier of U2 & f is one-to-one

    proof

      thus f is_isomorphism implies f is_homomorphism & ( rng f) = the carrier of U2 & f is one-to-one

      proof

        assume f is_isomorphism ;

        then f is_monomorphism & f is_epimorphism ;

        hence thesis;

      end;

      assume f is_homomorphism & ( rng f) = the carrier of U2 & f is one-to-one;

      then f is_monomorphism & f is_epimorphism ;

      hence thesis;

    end;

    theorem :: ALG_1:8

    

     Th8: f is_isomorphism implies ( dom f) = the carrier of U1 & ( rng f) = the carrier of U2

    proof

      assume f is_isomorphism ;

      then f is_epimorphism ;

      hence thesis by FUNCT_2:def 1;

    end;

    theorem :: ALG_1:9

    

     Th9: for h be Function of U1, U2, h1 be Function of U2, U1 st h is_isomorphism & h1 = (h " ) holds h1 is_homomorphism

    proof

      let h be Function of U1, U2, h1 be Function of U2, U1;

      assume that

       A1: h is_isomorphism and

       A2: h1 = (h " );

      

       A3: h is one-to-one by A1, Th7;

      

       A4: h is_homomorphism by A1, Th7;

      then

       A5: (U1,U2) are_similar ;

      then

       A6: ( signature U1) = ( signature U2);

      

       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

        let n;

        assume

         A11: n in ( dom the charact of U2);

        let o2, o1;

        assume

         A12: o2 = (the charact of U2 . n) & o1 = (the charact of U1 . n);

        let x be FinSequence of U2;

        defpred P[ set, set] means (h . $2) = (x . $1);

        

         A13: ( dom x) = ( Seg ( len x)) by FINSEQ_1:def 3;

        

         A14: for m be Nat st m in ( Seg ( len x)) holds ex a be Element of U1 st P[m, a]

        proof

          let m be Nat;

          assume m in ( Seg ( len x));

          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 be object such that

           A15: a in ( dom h) and

           A16: (h . a) = (x . m) by A10, FUNCT_1:def 3;

          reconsider a as Element of U1 by A15;

          take a;

          thus thesis by A16;

        end;

        consider p be FinSequence of U1 such that

         A17: ( dom p) = ( Seg ( len x)) & for m be Nat st m in ( Seg ( len x)) holds P[m, (p . m)] from FINSEQ_1:sch 5( A14);

        

         A18: ( dom (h * p)) = ( dom p) by FINSEQ_3: 120;

        now

          let n be Nat;

          assume

           A19: n in ( dom x);

          

          hence (x . n) = (h . (p . n)) by A17, A13

          .= ((h * p) . n) by A17, A13, A18, A19, FINSEQ_3: 120;

        end;

        then

         A20: x = (h * p) by A17, A13, A18;

        

         A21: ( len p) = ( len x) by A17, FINSEQ_1:def 3;

        assume x in ( dom o2);

        then x in (( arity o2) -tuples_on the carrier of U2) by MARGREL1: 22;

        then x in { s where s be Element of (the carrier of U2 * ) : ( len s) = ( arity o2) } by FINSEQ_2:def 4;

        then

         A22: ex s be 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 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 be 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;

        

         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;

      end;

      hence thesis by A5;

    end;

    theorem :: ALG_1:10

    

     Th10: for h be Function of U1, U2, h1 be Function of U2, U1 st h is_isomorphism & h1 = (h " ) holds h1 is_isomorphism

    proof

      let h be Function of U1, U2, h1 be Function of U2, U1;

      assume that

       A1: h is_isomorphism and

       A2: h1 = (h " );

      

       A3: h1 is_homomorphism 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 thesis by A2, A4, A3, Th7;

    end;

    theorem :: ALG_1:11

    

     Th11: for h be Function of U1, U2, h1 be Function of U2, U3 st h is_isomorphism & h1 is_isomorphism holds (h1 * h) is_isomorphism

    proof

      let h be Function of U1, U2, h1 be Function of U2, U3;

      assume that

       A1: h is_isomorphism and

       A2: h1 is_isomorphism ;

      ( 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 & h1 is_homomorphism by A1, A2, Th7;

      then

       A4: (h1 * h) is_homomorphism by Th6;

      h is one-to-one & h1 is one-to-one by A1, A2, Th7;

      hence thesis by A3, A4, Th7;

    end;

    theorem :: ALG_1:12

    (U1,U1) are_isomorphic

    proof

      set i = ( id the carrier of U1);

      i is_homomorphism & ( rng i) = the carrier of U1 by Th5;

      then i is_isomorphism by Th7;

      hence thesis;

    end;

    theorem :: ALG_1:13

    (U1,U2) are_isomorphic implies (U2,U1) are_isomorphic

    proof

      assume (U1,U2) are_isomorphic ;

      then

      consider f such that

       A1: f is_isomorphism ;

      f is_monomorphism by A1;

      then

       A2: f is one-to-one;

      

      then

       A3: ( rng (f " )) = ( dom f) by FUNCT_1: 33

      .= the carrier of U1 by FUNCT_2:def 1;

      

       A4: f is_epimorphism by A1;

      ( dom (f " )) = ( rng f) by A2, FUNCT_1: 33

      .= the carrier of U2 by A4;

      then

      reconsider g = (f " ) as Function of U2, U1 by A3, FUNCT_2:def 1, RELSET_1: 4;

      take g;

      thus thesis by A1, Th10;

    end;

    theorem :: ALG_1:14

    (U1,U2) are_isomorphic & (U2,U3) are_isomorphic implies (U1,U3) are_isomorphic

    proof

      assume (U1,U2) are_isomorphic ;

      then

      consider f such that

       A1: f is_isomorphism ;

      assume (U2,U3) are_isomorphic ;

      then

      consider g be Function of U2, U3 such that

       A2: g is_isomorphism ;

      (g * f) is_isomorphism by A1, A2, Th11;

      hence thesis;

    end;

    definition

      let U1, U2, f;

      assume

       A1: f is_homomorphism ;

      :: ALG_1:def6

      func Image f -> strict SubAlgebra of U2 means

      : Def6: the carrier of it = (f .: the carrier of U1);

      existence

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

        A is opers_closed

        proof

          let o2 be operation of U2;

          consider n be 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;

          assume

           A5: ( len s) = ( arity o2);

          defpred P[ object, object] means (f . $2) = (s . $1);

          

           A6: for x be object st x in ( dom s) holds ex y be object st y in the carrier of U1 & P[x, y]

          proof

            let x be object;

            assume

             A7: x in ( dom s);

            then

            reconsider x0 = x as Element of NAT ;

            (s . x0) in A by A7, FINSEQ_2: 11;

            then

            consider y be object 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;

            thus thesis by A8, A9;

          end;

          consider s1 be Function such that

           A10: ( dom s1) = ( dom s) & ( rng s1) c= the carrier of U1 & for x be object st x in ( dom s) holds P[x, (s1 . x)] from FUNCT_1:sch 6( A6);

          ( dom s1) = ( Seg ( len s)) by A10, FINSEQ_1:def 3;

          then

          reconsider s1 as FinSequence by FINSEQ_1:def 2;

          reconsider s1 as FinSequence of U1 by A10, FINSEQ_1:def 4;

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

          then

           A14: ( signature U1) = ( signature U2);

          

           A15: ( dom ( signature U1)) = ( dom ( signature U2)) by A13;

          

           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

            let m be Nat;

            assume

             A20: m in ( dom s);

            then (f . (s1 . m)) = (s . m) by A10;

            hence ((f * s1) . m) = (s . m) by A18, A19, A20, FINSEQ_3: 120;

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

          hence thesis by A2, A21, A25, FUNCT_1:def 6;

        end;

        then B = UAStr (# A, ( Opers (U2,A)) #) by UNIALG_2:def 8;

        hence thesis;

      end;

      uniqueness

      proof

        let A,B be strict SubAlgebra of U2;

        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 thesis by UNIALG_2:def 7;

      end;

    end

    theorem :: ALG_1:15

    for h be Function of U1, U2 st h is_homomorphism holds ( rng h) = the carrier of ( Image h)

    proof

      let h be Function of U1, U2;

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

      hence thesis by A1, Def6;

    end;

    theorem :: ALG_1:16

    for U2 be strict Universal_Algebra, f be Function of U1, U2 st f is_homomorphism holds f is_epimorphism iff ( Image f) = U2

    proof

      let U2 be strict Universal_Algebra;

      let f be Function of U1, U2;

      assume

       A1: f is_homomorphism ;

      thus f is_epimorphism implies ( Image f) = U2

      proof

        reconsider B = the carrier of ( Image f) as non empty Subset of U2 by UNIALG_2:def 7;

        assume f is_epimorphism ;

        

        then

         A2: the carrier of U2 = ( rng f)

        .= (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 thesis by A2, Th1;

      end;

      assume ( Image f) = 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 thesis by A1;

    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;

      :: ALG_1:def7

      mode Congruence of U1 -> Equivalence_Relation of U1 means

      : Def7: for n, o1 st n in ( dom the charact of U1) & o1 = (the charact of U1 . n) holds for x,y be 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

      proof

        reconsider P = ( id the carrier of U1) as Equivalence_Relation of U1;

        take P;

        let n, o1;

        assume that n in ( dom the charact of U1) and o1 = (the charact of U1 . n);

        let x,y be FinSequence of U1;

        assume that

         A1: x in ( dom o1) and y in ( dom o1) and

         A2: [x, y] in ( ExtendRel 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 thesis by A3, RELAT_1:def 10;

      end;

    end

    reserve E for Congruence of U1;

    definition

      let U1 be Universal_Algebra, E be Congruence of U1, o be operation of U1;

      :: ALG_1:def8

      func QuotOp (o,E) -> homogeneous quasi_total non empty PartFunc of (( Class E) * ), ( Class E) means

      : Def8: ( dom it ) = (( arity o) -tuples_on ( Class E)) & for y be FinSequence of ( Class E) st y in ( dom it ) holds for x be FinSequence of the carrier of U1 st x is_representatives_FS y holds (it . y) = ( Class (E,(o . x)));

      existence

      proof

        defpred P[ object, object] means for y be FinSequence of ( Class E) st y = $1 holds for x be 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 be object st e in X holds ex u be object st u in ( Class E) & P[e, u]

        proof

          let e be object;

          

           A2: ( dom o) = (( arity o) -tuples_on the carrier of U1) by MARGREL1: 22

          .= { q where q be Element of (the carrier of U1 * ) : ( len q) = ( arity o) } by FINSEQ_2:def 4;

          assume e in X;

          then e in { s where s be Element of (( Class E) * ) : ( len s) = ( arity o) } by FINSEQ_2:def 4;

          then

          consider s be Element of (( Class E) * ) such that

           A3: s = e and

           A4: ( len s) = ( arity o);

          consider x be FinSequence of the carrier of U1 such that

           A5: x is_representatives_FS s by FINSEQ_3: 122;

          take y = ( Class (E,(o . x)));

          

           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;

          let a be FinSequence of ( Class E);

          assume

           A9: a = e;

          let b be FinSequence of the carrier of U1;

          assume

           A10: b is_representatives_FS a;

          then

           A11: ( len b) = ( arity o) by A3, A4, A9, FINSEQ_3:def 4;

          for m st m in ( dom x) holds [(x . m), (b . m)] in E

          proof

            let m;

            assume

             A12: m in ( dom x);

            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 thesis by A13, EQREL_1: 35;

          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 be 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 thesis by A8, EQREL_1: 35;

        end;

        consider F be Function such that

         A15: ( dom F) = X & ( rng F) c= ( Class E) & for e be object st e in X holds P[e, (F . e)] from FUNCT_1:sch 6( A1);

        X in the set of all (m -tuples_on ( Class E));

        then X c= ( union the set of all (m -tuples_on ( Class E))) by ZFMISC_1: 74;

        then X c= (( Class E) * ) by FINSEQ_2: 108;

        then

        reconsider F as PartFunc of (( Class E) * ), ( Class E) by A15, RELSET_1: 4;

        

         A16: ( dom F) = { t where t be Element of (( Class E) * ) : ( len t) = ( arity o) } by A15, FINSEQ_2:def 4;

        

         A17: for x,y be 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);

          assume that

           A18: ( len x) = ( len y) and

           A19: x in ( dom F);

          

           A20: y is Element of (( Class E) * ) by FINSEQ_1:def 11;

          ex t1 be Element of (( Class E) * ) st x = t1 & ( len t1) = ( arity o) by A16, A19;

          hence thesis by A16, A18, A20;

        end;

        

         A21: ex x be FinSequence st x in ( dom F)

        proof

          set a = the Element of X;

          a in X;

          hence ex x be FinSequence st x in ( dom F) by A15;

        end;

        ( dom F) is with_common_domain

        proof

          let x,y be FinSequence;

          assume x in ( dom F) & y in ( dom F);

          then (ex t1 be Element of (( Class E) * ) st x = t1 & ( len t1) = ( arity o)) & ex t2 be Element of (( Class E) * ) st y = t2 & ( len t2) = ( arity o) by A16;

          hence thesis;

        end;

        then

        reconsider F as homogeneous quasi_total non empty PartFunc of (( Class E) * ), ( Class E) by A17, A21, MARGREL1:def 21, MARGREL1:def 22;

        take F;

        thus ( dom F) = (( arity o) -tuples_on ( Class E)) by A15;

        let y be FinSequence of ( Class E);

        assume

         A22: y in ( dom F);

        let x be FinSequence of the carrier of U1;

        assume x is_representatives_FS y;

        hence thesis by A15, A22;

      end;

      uniqueness

      proof

        let F,G be homogeneous quasi_total non empty PartFunc of (( Class E) * ), ( Class E);

        assume that

         A23: ( dom F) = (( arity o) -tuples_on ( Class E)) and

         A24: for y be FinSequence of ( Class E) st y in ( dom F) holds for x be 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 be FinSequence of ( Class E) st y in ( dom G) holds for x be FinSequence of the carrier of U1 st x is_representatives_FS y holds (G . y) = ( Class (E,(o . x)));

        for a be object st a in ( dom F) holds (F . a) = (G . a)

        proof

          let a be object;

          assume

           A27: a in ( dom F);

          then

          reconsider b = a as FinSequence of ( Class E) by FINSEQ_1:def 11;

          consider x be 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 thesis by A23, A25, A26, A27, A28;

        end;

        hence thesis by A23, A25;

      end;

    end

    definition

      let U1, E;

      :: ALG_1:def9

      func QuotOpSeq (U1,E) -> PFuncFinSequence of ( Class E) means

      : Def9: ( len it ) = ( len the charact of U1) & for n st n in ( dom it ) holds for o1 st (the charact of U1 . n) = o1 holds (it . n) = ( QuotOp (o1,E));

      existence

      proof

        defpred P[ set, set] means for o be Element of ( Operations U1) st o = (the charact of U1 . $1) holds $2 = ( QuotOp (o,E));

        

         A1: for n be Nat st n in ( Seg ( len the charact of U1)) holds ex x be Element of ( PFuncs ((( Class E) * ),( Class E))) st P[n, x]

        proof

          let n be Nat;

          assume n in ( Seg ( len the charact of U1));

          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;

          thus thesis;

        end;

        consider p be FinSequence of ( PFuncs ((( Class E) * ),( Class E))) such that

         A2: ( dom p) = ( Seg ( len the charact of U1)) & for n be Nat st n in ( Seg ( len the charact of U1)) holds P[n, (p . n)] from FINSEQ_1:sch 5( A1);

        reconsider p as PFuncFinSequence of ( Class E);

        take p;

        thus ( len p) = ( len the charact of U1) by A2, FINSEQ_1:def 3;

        let n;

        assume n in ( dom p);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let F,G be PFuncFinSequence of ( Class E);

        assume that

         A3: ( len F) = ( len the charact of U1) and

         A4: for n st n in ( dom F) holds for o1 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 st n in ( dom G) holds for o1 st (the charact of U1 . n) = o1 holds (G . n) = ( QuotOp (o1,E));

        now

          let n be Nat;

          assume

           A7: n in ( dom F);

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

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

    end

    definition

      let U1, E;

      :: ALG_1:def10

      func QuotUnivAlg (U1,E) -> strict Universal_Algebra equals UAStr (# ( Class E), ( QuotOpSeq (U1,E)) #);

      coherence

      proof

        set UU = UAStr (# ( Class E), ( QuotOpSeq (U1,E)) #);

        for n be Nat, h be 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, h be PartFunc of (( Class E) * ), ( Class E);

          assume that

           A1: n in ( dom ( QuotOpSeq (U1,E))) and

           A2: h = (( QuotOpSeq (U1,E)) . n);

          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 thesis by A2;

        end;

        then

         A3: the charact of UU is homogeneous;

        for n be Nat, h be 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, h be PartFunc of (( Class E) * ), ( Class E);

          assume that

           A4: n in ( dom ( QuotOpSeq (U1,E))) and

           A5: h = (( QuotOpSeq (U1,E)) . n);

          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 thesis by A5;

        end;

        then

         A6: the charact of UU is quasi_total;

        for n be object st n in ( dom ( QuotOpSeq (U1,E))) holds (( QuotOpSeq (U1,E)) . n) is non empty

        proof

          let n be object;

          assume

           A7: n in ( dom ( QuotOpSeq (U1,E)));

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

        end;

        then

         A9: the charact of UU is non-empty by FUNCT_1:def 9;

        the charact of UU <> {}

        proof

          assume

           A10: the charact of UU = {} ;

          ( len the charact of UU) = ( len the charact of U1) by Def9;

          hence contradiction by A10;

        end;

        hence thesis by A3, A6, A9, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;

      end;

    end

    definition

      let U1, E;

      :: ALG_1:def11

      func Nat_Hom (U1,E) -> Function of U1, ( QuotUnivAlg (U1,E)) means

      : Def11: for u be Element of U1 holds (it . u) = ( Class (E,u));

      existence

      proof

        defpred P[ Element of U1, set] means $2 = ( Class (E,$1));

        

         A1: for x be Element of U1 holds ex y be Element of ( QuotUnivAlg (U1,E)) st P[x, y]

        proof

          let x be Element of U1;

          reconsider y = ( Class (E,x)) as Element of ( QuotUnivAlg (U1,E)) by EQREL_1:def 3;

          take y;

          thus thesis;

        end;

        consider f be Function of U1, ( QuotUnivAlg (U1,E)) such that

         A2: for x be Element of U1 holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of U1, ( QuotUnivAlg (U1,E));

        assume that

         A3: for u be Element of U1 holds (f . u) = ( Class (E,u)) and

         A4: for u be Element of U1 holds (g . u) = ( Class (E,u));

        now

          let u be Element of U1;

          (f . u) = ( Class (E,u)) by A3;

          hence (f . u) = (g . u) by A4;

        end;

        hence thesis;

      end;

    end

    theorem :: ALG_1:17

    

     Th17: for U1, E holds ( Nat_Hom (U1,E)) is_homomorphism

    proof

      let U1, E;

      set f = ( Nat_Hom (U1,E)), u1 = the carrier of U1, 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

        let n be Nat;

        assume

         A5: n in ( dom ( signature U1));

        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 homogeneous quasi_total non empty PartFunc of (qu * ), qu;

        consider b be object such that

         A7: b in ( dom cl) by XBOOLE_0:def 1;

        reconsider b as Element of (qu * ) by A7;

        ( dom ( QuotOp (o1,E))) = (( arity o1) -tuples_on ( Class E)) by Def8;

        then b in { w where w be Element of (( Class E) * ) : ( len w) = ( arity o1) } by A7, FINSEQ_2:def 4;

        then ex w be 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;

      end;

      hence ( signature U1) = ( signature ( QuotUnivAlg (U1,E))) by A3, A4, A1, FINSEQ_2: 9;

      let n;

      assume n in ( dom the charact of U1);

      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, o2 be operation of ( QuotUnivAlg (U1,E));

      assume (the charact of U1 . n) = o1 & o2 = (the charact of ( QuotUnivAlg (U1,E)) . n);

      then

       A10: o2 = ( QuotOp (o1,E)) by A9, Def9;

      let x be FinSequence of U1;

      reconsider x1 = x as Element of (u1 * ) by FINSEQ_1:def 11;

      reconsider fx = (f * x) as FinSequence of ( Class E);

      reconsider fx as Element of (( Class E) * ) by FINSEQ_1:def 11;

      

       A11: ( len (f * x)) = ( len x) by FINSEQ_3: 120;

      now

        let m;

        assume

         A12: m in ( dom x);

        then

         A13: m in ( dom (f * x)) by FINSEQ_3: 120;

        (x . m) in ( rng x) by A12, FUNCT_1:def 3;

        then

        reconsider xm = (x . m) as Element of u1;

        

        thus ( Class (E,(x . m))) = (f . xm) by Def11

        .= (fx . m) by A13, FINSEQ_3: 120;

      end;

      then

       A14: x is_representatives_FS fx by A11, FINSEQ_3:def 4;

      assume

       A15: x in ( dom o1);

      then (o1 . x) in ( rng o1) by FUNCT_1:def 3;

      then

      reconsider ox = (o1 . x) as Element of u1;

      ( dom o1) = (( arity o1) -tuples_on u1) by MARGREL1: 22

      .= { p where p be Element of (u1 * ) : ( len p) = ( arity o1) } by FINSEQ_2:def 4;

      then

       A16: ex p be Element of (u1 * ) st p = x1 & ( len p) = ( arity o1) by A15;

      

       A17: (f . (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 be Element of (( Class E) * ) : ( len q) = ( arity o1) } by FINSEQ_2:def 4;

      then fx in ( dom ( QuotOp (o1,E))) by A16, A11;

      hence thesis by A17, A10, A14, Def8;

    end;

    theorem :: ALG_1:18

    for U1, E holds ( Nat_Hom (U1,E)) is_epimorphism

    proof

      let U1, E;

      set f = ( Nat_Hom (U1,E)), qa = ( QuotUnivAlg (U1,E)), cqa = the carrier of qa, u1 = the carrier of U1;

      thus f is_homomorphism by Th17;

      thus ( rng f) c= cqa;

      let x be object;

      assume

       A1: x in cqa;

      then

      reconsider x1 = x as Subset of u1;

      consider y be object such that

       A2: y in u1 and

       A3: x1 = ( Class (E,y)) by A1, EQREL_1:def 3;

      reconsider y as Element of u1 by A2;

      ( dom f) = u1 by FUNCT_2:def 1;

      then (f . y) in ( rng f) by FUNCT_1:def 3;

      hence thesis by A3, Def11;

    end;

    definition

      let U1, U2;

      let f be Function of U1, U2;

      assume

       A1: f is_homomorphism ;

      :: ALG_1:def12

      func Cng (f) -> Congruence of U1 means

      : Def12: for a,b be Element of U1 holds [a, b] in it iff (f . a) = (f . b);

      existence

      proof

        defpred P[ set, set] means (f . $1) = (f . $2);

        set u1 = the carrier of U1;

        consider R be Relation of u1, u1 such that

         A2: for x,y be Element of u1 holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

        R is_reflexive_in u1

        proof

          let x be object;

          assume x in u1;

          then

          reconsider x1 = x as Element of u1;

          (f . x1) = (f . x1);

          hence thesis by A2;

        end;

        then

         A3: ( dom R) = u1 & ( field R) = u1 by ORDERS_1: 13;

        

         A4: R is_transitive_in u1

        proof

          let x,y,z be object;

          assume that

           A5: x in u1 & y in u1 & z in u1 and

           A6: [x, y] in R & [y, z] in R;

          reconsider x1 = x, y1 = y, z1 = z as Element of u1 by A5;

          (f . x1) = (f . y1) & (f . y1) = (f . z1) by A2, A6;

          hence thesis by A2;

        end;

        R is_symmetric_in u1

        proof

          let x,y be object;

          assume that

           A7: x in u1 & y in u1 and

           A8: [x, y] in R;

          reconsider x1 = x, y1 = y as Element of u1 by A7;

          (f . x1) = (f . y1) by A2, A8;

          hence thesis by A2;

        end;

        then

        reconsider R as Equivalence_Relation of U1 by A3, A4, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

        now

          (U1,U2) are_similar by A1;

          then

           A9: ( signature U1) = ( signature U2);

          let n be Nat, o be operation of U1;

          assume that

           A10: n in ( dom the charact of U1) and

           A11: o = (the charact of U1 . n);

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

          assume that

           A12: x in ( dom o) & y in ( dom o) and

           A13: [x, y] in ( ExtendRel 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 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

            let m be Nat;

            assume

             A19: m in ( dom (f * y));

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

          end;

          (f . (o . x)) = (o2 . (f * x)) & (f . (o . y)) = (o2 . (f * y)) by A1, A10, A11, A12;

          then (f . ox) = (f . oy) by A14, A17, A15, A18, FINSEQ_2: 9;

          hence [(o . x), (o . y)] in R by A2;

        end;

        then

        reconsider R as Congruence of U1 by Def7;

        take R;

        let a,b be Element of u1;

        thus [a, b] in R implies (f . a) = (f . b) by A2;

        assume (f . a) = (f . b);

        hence thesis by A2;

      end;

      uniqueness

      proof

        set u1 = the carrier of U1;

        let X,Y be Congruence of U1;

        assume that

         A23: for a,b be Element of U1 holds [a, b] in X iff (f . a) = (f . b) and

         A24: for a,b be Element of U1 holds [a, b] in Y iff (f . a) = (f . b);

        for x,y be object holds [x, y] in X iff [x, y] in Y

        proof

          let x,y be object;

          thus [x, y] in X implies [x, y] in Y

          proof

            assume

             A25: [x, y] in X;

            then

            reconsider x1 = x, y1 = y as Element of u1 by ZFMISC_1: 87;

            (f . x1) = (f . y1) by A23, A25;

            hence thesis by A24;

          end;

          assume

           A26: [x, y] in Y;

          then

          reconsider x1 = x, y1 = y as Element of u1 by ZFMISC_1: 87;

          (f . x1) = (f . y1) by A24, A26;

          hence thesis by A23;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let U1,U2 be Universal_Algebra, f be Function of U1, U2;

      assume

       A1: f is_homomorphism ;

      :: ALG_1:def13

      func HomQuot (f) -> Function of ( QuotUnivAlg (U1,( Cng f))), U2 means

      : Def13: for a be Element of U1 holds (it . ( Class (( Cng f),a))) = (f . a);

      existence

      proof

        set qa = ( QuotUnivAlg (U1,( Cng f))), cqa = the carrier of qa, u1 = the carrier of U1, u2 = the carrier of U2;

        defpred P[ object, object] means for a be Element of u1 st $1 = ( Class (( Cng f),a)) holds $2 = (f . a);

        

         A2: for x be object st x in cqa holds ex y be object st y in u2 & P[x, y]

        proof

          let x be object;

          assume

           A3: x in cqa;

          then

          reconsider x1 = x as Subset of u1;

          consider a be object such that

           A4: a in u1 and

           A5: x1 = ( Class (( Cng f),a)) by A3, EQREL_1:def 3;

          reconsider a as Element of u1 by A4;

          take y = (f . a);

          thus y in u2;

          let b be Element of u1;

          assume x = ( Class (( Cng 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 thesis by A1, Def12;

        end;

        consider F be Function such that

         A6: ( dom F) = cqa & ( rng F) c= u2 & for x be object st x in cqa holds P[x, (F . x)] from FUNCT_1:sch 6( A2);

        reconsider F as Function of qa, U2 by A6, FUNCT_2:def 1, RELSET_1: 4;

        take F;

        let a be Element of u1;

        ( Class (( Cng f),a)) in ( Class ( Cng f)) by EQREL_1:def 3;

        hence thesis by A6;

      end;

      uniqueness

      proof

        set qa = ( QuotUnivAlg (U1,( Cng f))), cqa = the carrier of qa, u1 = the carrier of U1;

        let F,G be Function of qa, U2;

        assume that

         A7: for a be Element of u1 holds (F . ( Class (( Cng f),a))) = (f . a) and

         A8: for a be Element of u1 holds (G . ( Class (( Cng f),a))) = (f . a);

        let x be Element of cqa;

        x in cqa;

        then

        reconsider x1 = x as Subset of u1;

        consider a be object such that

         A9: a in u1 & x1 = ( Class (( Cng f),a)) by EQREL_1:def 3;

        

        thus (F . x) = (f . a) by A7, A9

        .= (G . x) by A8, A9;

      end;

    end

    theorem :: ALG_1:19

    

     Th19: f is_homomorphism implies ( HomQuot f) is_homomorphism & ( HomQuot f) is_monomorphism

    proof

      set qa = ( QuotUnivAlg (U1,( Cng f))), cqa = the carrier of qa, u1 = the carrier of U1, F = ( HomQuot f);

      assume

       A1: f is_homomorphism ;

      thus

       A2: F is_homomorphism

      proof

        ( Nat_Hom (U1,( Cng f))) is_homomorphism by Th17;

        then (U1,qa) are_similar ;

        then

         A3: ( signature U1) = ( signature qa);

        (U1,U2) are_similar by A1;

        then ( signature U2) = ( signature qa) by A3;

        hence (qa,U2) are_similar ;

        let n;

        assume

         A4: n in ( dom the charact of qa);

        

         A5: ( len ( signature U1)) = ( len the charact of U1) & ( len ( signature qa)) = ( len the charact of qa) by UNIALG_1:def 4;

        

         A6: ( dom the charact of qa) = ( Seg ( len the charact of qa)) & ( 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 u1) by MARGREL1: 22

        .= { p where p be Element of (u1 * ) : ( len p) = ( arity o1) } by FINSEQ_2:def 4;

        let oq be operation of qa, o2 be operation of U2;

        assume that

         A8: oq = (the charact of qa . n) and

         A9: o2 = (the charact of U2 . n);

        let x be FinSequence of qa;

        assume

         A10: x in ( dom oq);

        reconsider x1 = x as FinSequence of ( Class ( Cng f));

        reconsider x1 as Element of (( Class ( Cng f)) * ) by FINSEQ_1:def 11;

        consider y be FinSequence of U1 such that

         A11: y is_representatives_FS x1 by FINSEQ_3: 122;

        reconsider y as Element of (u1 * ) by FINSEQ_1:def 11;

        

         A12: ( len x1) = ( len y) by A11, FINSEQ_3:def 4;

        then

         A13: ( len (F * x)) = ( len y) by FINSEQ_3: 120;

        

         A14: ( len y) = ( len (f * y)) by FINSEQ_3: 120;

         A15:

        now

          let m be Nat;

          assume

           A16: m in ( Seg ( len y));

          then

           A17: m in ( dom (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 u1 by FINSEQ_2: 11;

          (x1 . m) = ( Class (( Cng f),(y . m))) by A11, A19, FINSEQ_3:def 4;

          

          hence ((F * x) . m) = (F . ( Class (( Cng f),ym))) by A17, FINSEQ_3: 120

          .= (f . (y . m)) by A1, Def13

          .= ((f * y) . m) by A18, FINSEQ_3: 120;

        end;

        ( dom (F * x)) = ( Seg ( len y)) by A13, FINSEQ_1:def 3;

        then

         A20: (o2 . (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 be Element of (( Class ( Cng f)) * ) : ( len w) = ( arity o1) } by FINSEQ_2:def 4;

        then ex w be 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 u1;

        (F . (oq . x)) = (F . ( Class (( Cng f),o1y))) by A10, A11, A21, Def8

        .= (f . (o1 . y)) by A1, Def13;

        hence thesis by A1, A3, A4, A9, A6, A5, A22, A20;

      end;

      

       A23: ( dom F) = cqa by FUNCT_2:def 1;

      F is one-to-one

      proof

        let x,y be object;

        assume that

         A24: x in ( dom F) and

         A25: y in ( dom F) and

         A26: (F . x) = (F . y);

        reconsider x1 = x, y1 = y as Subset of u1 by A23, A24, A25;

        consider a be object such that

         A27: a in u1 and

         A28: x1 = ( Class (( Cng f),a)) by A24, EQREL_1:def 3;

        reconsider a as Element of u1 by A27;

        consider b be object such that

         A29: b in u1 and

         A30: y1 = ( Class (( Cng f),b)) by A25, EQREL_1:def 3;

        reconsider b as Element of u1 by A29;

        

         A31: (F . y1) = (f . b) by A1, A30, Def13;

        (F . x1) = (f . a) by A1, A28, Def13;

        then [a, b] in ( Cng f) by A1, A26, A31, Def12;

        hence thesis by A28, A30, EQREL_1: 35;

      end;

      hence thesis by A2;

    end;

    ::$Notion-Name

    theorem :: ALG_1:20

    

     Th20: f is_epimorphism implies ( HomQuot f) is_isomorphism

    proof

      set qa = ( QuotUnivAlg (U1,( Cng f))), u1 = the carrier of U1, u2 = the carrier of U2, F = ( HomQuot f);

      assume

       A1: f is_epimorphism ;

      then

       A2: f is_homomorphism ;

      then F is_monomorphism by Th19;

      then

       A3: F is one-to-one;

      

       A4: ( rng f) = u2 by A1;

      

       A5: ( rng F) = u2

      proof

        thus ( rng F) c= u2;

        let x be object;

        assume x in u2;

        then

        consider y be object such that

         A6: y in ( dom f) and

         A7: (f . y) = x by A4, FUNCT_1:def 3;

        reconsider y as Element of u1 by A6;

        set u = ( Class (( Cng f),y));

        

         A8: ( dom F) = the carrier of qa & u in ( Class ( Cng f)) by EQREL_1:def 3, FUNCT_2:def 1;

        (F . u) = x by A2, A7, Def13;

        hence thesis by A8, FUNCT_1:def 3;

      end;

      F is_homomorphism by A2, Th19;

      hence thesis by A3, A5, Th7;

    end;

    theorem :: ALG_1:21

    f is_epimorphism implies (( QuotUnivAlg (U1,( Cng f))),U2) are_isomorphic

    proof

      assume

       A1: f is_epimorphism ;

      take ( HomQuot f);

      thus thesis by A1, Th20;

    end;