ringcat1.miz

    begin

    reserve x,y for set;

    reserve D for non empty set;

    reserve UN for Universe;

    definition

      let G,H be non empty doubleLoopStr;

      let IT be Function of G, H;

      :: RINGCAT1:def1

      attr IT is linear means IT is additive multiplicative unity-preserving;

    end

    registration

      let G,H be non empty doubleLoopStr;

      cluster linear -> additive multiplicative unity-preserving for Function of G, H;

      coherence ;

      cluster additive multiplicative unity-preserving -> linear for Function of G, H;

      coherence ;

    end

    theorem :: RINGCAT1:1



     Th1: for G1,G2,G3 be non empty doubleLoopStr, f be Function of G1, G2, g be Function of G2, G3 st f is linear & g is linear holds (g * f) is linear

    proof

      let G1,G2,G3 be non empty doubleLoopStr, f be Function of G1, G2, g be Function of G2, G3 such that

       A1: f is additive multiplicative unity-preserving and

       A2: g is additive multiplicative unity-preserving;

      set h = (g * f);

      thus h is additive

      proof

        let x,y be Scalar of G1;



         A3: (g . (f . x)) = (h . x) & (g . (f . y)) = (h . y) by FUNCT_2: 15;



        thus (h . (x + y)) = (g . (f . (x + y))) by FUNCT_2: 15

        .= (g . ((f . x) + (f . y))) by A1

        .= ((h . x) + (h . y)) by A2, A3;

      end;

      thus h is multiplicative

      proof

        let x,y be Scalar of G1;



         A4: (g . (f . x)) = (h . x) & (g . (f . y)) = (h . y) by FUNCT_2: 15;



        thus (h . (x * y)) = (g . (f . (x * y))) by FUNCT_2: 15

        .= (g . ((f . x) * (f . y))) by A1

        .= ((h . x) * (h . y)) by A2, A4;

      end;



      thus (h . ( 1_ G1)) = (g . (f . ( 1_ G1))) by FUNCT_2: 15

      .= (g . ( 1_ G2)) by A1

      .= ( 1_ G3) by A2;

    end;

    definition

      struct RingMorphismStr (# the Dom, Cod -> Ring,

the Fun -> Function of the Dom, the Cod #)

       attr strict strict;

    end

    reserve f for RingMorphismStr;

    definition

      let f;

      :: RINGCAT1:def2

      func dom (f) -> Ring equals the Dom of f;

      coherence ;

      :: RINGCAT1:def3

      func cod (f) -> Ring equals the Cod of f;

      coherence ;

      :: RINGCAT1:def4

      func fun (f) -> Function of the Dom of f, the Cod of f equals the Fun of f;

      coherence ;

    end

    reserve G,H,G1,G2,G3,G4 for Ring;



     Lm1: for G be non empty doubleLoopStr holds ( id G) is linear

    proof

      let G be non empty doubleLoopStr;

      set f = ( id G);

      thus f is additive;

      thus f is multiplicative

      proof

        let x,y be Scalar of G;

        (f . (x * y)) = (x * y) & (f . x) = x by FUNCT_1: 18;

        hence thesis by FUNCT_1: 18;

      end;

      thus (f . ( 1_ G)) = ( 1_ G) by FUNCT_1: 18;

    end;

    registration

      let G be non empty doubleLoopStr;

      cluster ( id G) -> linear;

      coherence by Lm1;

    end

    definition

      let IT be RingMorphismStr;

      :: RINGCAT1:def5

      attr IT is RingMorphism-like means

      : Def5: ( fun IT) is linear;

    end

    registration

      cluster strict RingMorphism-like for RingMorphismStr;

      existence

      proof

        set G = the Ring;

        set i = RingMorphismStr (# G, G, ( id G) #);

        ( fun i) = ( id G);

        hence thesis by Def5;

      end;

    end

    definition

      mode RingMorphism is RingMorphism-like RingMorphismStr;

    end

    definition

      let G;

      :: RINGCAT1:def6

      func ID G -> RingMorphism equals RingMorphismStr (# G, G, ( id G) #);

      coherence

      proof

        set i = RingMorphismStr (# G, G, ( id G) #);

        ( fun i) = ( id G);

        hence thesis by Def5;

      end;

    end

    registration

      let G;

      cluster ( ID G) -> strict;

      coherence ;

    end

    reserve F for RingMorphism;

    definition

      let G, H;

      :: RINGCAT1:def7

      pred G <= H means ex F be RingMorphism st ( dom F) = G & ( cod F) = H;

      reflexivity

      proof

        let G;

        set i = ( ID G);

        take i;

        thus thesis;

      end;

    end



     Lm2: the RingMorphismStr of F is RingMorphism-like

    proof

      set S = the RingMorphismStr of F;



       A1: ( fun F) is linear by Def5;

      hence for x,y be Scalar of the Dom of S holds (( fun S) . (x + y)) = ((( fun S) . x) + (( fun S) . y)) by VECTSP_1:def 20;

      thus for x,y be Scalar of the Dom of S holds (( fun S) . (x * y)) = ((( fun S) . x) * (( fun S) . y)) by A1, GROUP_6:def 6;

      thus thesis by A1;

    end;

    definition

      let G, H;

      assume

       A1: G <= H;

      :: RINGCAT1:def8

      mode Morphism of G,H -> strict RingMorphism means

      : Def8: ( dom it ) = G & ( cod it ) = H;

      existence

      proof

        consider F be RingMorphism such that

         A2: ( dom F) = G & ( cod F) = H by A1;

        set S = the RingMorphismStr of F;



         A3: ( dom S) = G & ( cod S) = H by A2;

        S is RingMorphism by Lm2;

        hence thesis by A3;

      end;

    end

    registration

      let G, H;

      cluster strict for Morphism of G, H;

      existence

      proof

        set m = the Morphism of G, H;

        m is RingMorphism;

        hence thesis;

      end;

    end

    definition

      let G;

      :: original: ID

      redefine

      func ID G -> strict Morphism of G, G ;

      coherence

      proof

        set i = ( ID G);

        ( dom i) = G & ( cod i) = G;

        hence thesis by Def8;

      end;

    end



     Lm3: the Fun of F is linear

    proof

      the Fun of F = ( fun F);

      hence thesis by Def5;

    end;



     Lm4: for f be strict RingMorphismStr holds ( dom f) = G & ( cod f) = H & ( fun f) is linear implies f is Morphism of G, H

    proof

      let f be strict RingMorphismStr;

      assume that

       A1: ( dom f) = G and

       A2: ( cod f) = H and

       A3: ( fun f) is linear;

      reconsider f9 = f as RingMorphism by A3, Def5;

      ( dom f9) = G by A1;

      then G <= H by A2;

      then f9 is Morphism of G, H by A1, A2, Def8;

      hence thesis;

    end;



     Lm5: for f be Function of G, H st f is linear holds RingMorphismStr (# G, H, f #) is Morphism of G, H

    proof

      let f be Function of G, H such that

       A1: f is linear;

      set F = RingMorphismStr (# G, H, f #);



       A2: ( fun F) = f;

      ( dom F) = G & ( cod F) = H;

      hence thesis by A1, A2, Lm4;

    end;



     Lm6: for F be RingMorphism holds ex G, H st G <= H & ( dom F) = G & ( cod F) = H & the RingMorphismStr of F is Morphism of G, H

    proof

      let F be RingMorphism;

      reconsider S = the RingMorphismStr of F as RingMorphism by Lm2;

      set G = the Dom of F, H = the Cod of F;

      take G, H;

      ( dom F) = G & ( cod F) = H;

      then

       A1: G <= H;

      ( dom S) = G & ( cod S) = H;

      hence thesis by A1, Def8;

    end;

    theorem :: RINGCAT1:2



     Th2: for g,f be RingMorphism st ( dom g) = ( cod f) holds ex G1, G2, G3 st G1 <= G2 & G2 <= G3 & the RingMorphismStr of g is Morphism of G2, G3 & the RingMorphismStr of f is Morphism of G1, G2

    proof

      defpred P[ RingMorphism, RingMorphism] means ( dom $1) = ( cod $2);

      let g,f be RingMorphism such that

       A1: P[g, f];

      (ex G2, G3 st G2 <= G3 & ( dom g) = G2 & ( cod g) = G3 & the RingMorphismStr of g is Morphism of G2, G3) & ex G1,G29 be Ring st G1 <= G29 & ( dom f) = G1 & ( cod f) = G29 & the RingMorphismStr of f is Morphism of G1, G29 by Lm6;

      hence thesis by A1;

    end;

    theorem :: RINGCAT1:3



     Th3: for F be strict RingMorphism holds F is Morphism of ( dom F), ( cod F) & ( dom F) <= ( cod F)

    proof

      let F be strict RingMorphism;

      ex G, H st G <= H & ( dom F) = G & ( cod F) = H & F is Morphism of G, H by Lm6;

      hence thesis;

    end;



     Lm7: for F be Morphism of G, H st G <= H holds ex f be Function of G, H st F = RingMorphismStr (# G, H, f #) & f is linear

    proof

      let F be Morphism of G, H such that

       A1: G <= H;



       A2: the Cod of F = ( cod F)

      .= H by A1, Def8;



       A3: the Dom of F = ( dom F)

      .= G by A1, Def8;

      then

      reconsider f = the Fun of F as Function of G, H by A2;

      take f;

      thus thesis by A3, A2, Lm3;

    end;



     Lm8: for F be Morphism of G, H st G <= H holds ex f be Function of G, H st F = RingMorphismStr (# G, H, f #)

    proof

      let F be Morphism of G, H;

      assume G <= H;

      then

      consider f be Function of G, H such that

       A1: F = RingMorphismStr (# G, H, f #) and f is linear by Lm7;

      take f;

      thus thesis by A1;

    end;

    theorem :: RINGCAT1:4

    for F be strict RingMorphism holds ex G, H st ex f be Function of G, H st F is Morphism of G, H & F = RingMorphismStr (# G, H, f #) & f is linear

    proof

      let F be strict RingMorphism;

      consider G, H such that

       A1: G <= H and ( dom F) = G and ( cod F) = H and

       A2: F is Morphism of G, H by Lm6;

      reconsider F9 = F as Morphism of G, H by A2;

      consider f be Function of G, H such that

       A3: F9 = RingMorphismStr (# G, H, f #) & f is linear by A1, Lm7;

      take G, H, f;

      thus thesis by A3;

    end;

    definition

      let G,F be RingMorphism;

      assume

       A1: ( dom G) = ( cod F);

      :: RINGCAT1:def9

      func G * F -> strict RingMorphism means

      : Def9: for G1, G2, G3 holds for g be Function of G2, G3, f be Function of G1, G2 st the RingMorphismStr of G = RingMorphismStr (# G2, G3, g #) & the RingMorphismStr of F = RingMorphismStr (# G1, G2, f #) holds it = RingMorphismStr (# G1, G3, (g * f) #);

      existence

      proof

        consider G19,G29,G39 be Ring such that

         A2: G19 <= G29 and

         A3: G29 <= G39 & the RingMorphismStr of G is Morphism of G29, G39 and

         A4: the RingMorphismStr of F is Morphism of G19, G29 by A1, Th2;

        consider g9 be Function of G29, G39 such that

         A5: the RingMorphismStr of G = RingMorphismStr (# G29, G39, g9 #) and

         A6: g9 is linear by A3, Lm7;

        consider f9 be Function of G19, G29 such that

         A7: the RingMorphismStr of F = RingMorphismStr (# G19, G29, f9 #) and

         A8: f9 is linear by A2, A4, Lm7;

        (g9 * f9) is linear by A6, A8, Th1;

        then

        reconsider T9 = RingMorphismStr (# G19, G39, (g9 * f9) #) as strict RingMorphism by Lm5;

        take T9;

        thus thesis by A5, A7;

      end;

      uniqueness

      proof

        consider G19,G299 be Ring such that G19 <= G299 and

         A9: ( dom F) = G19 and

         A10: ( cod F) = G299 and

         A11: the RingMorphismStr of F is Morphism of G19, G299 by Lm6;

        reconsider F9 = the RingMorphismStr of F as Morphism of G19, G299 by A11;

        let S1,S2 be strict RingMorphism such that

         A12: for G1, G2, G3 holds for g be Function of G2, G3, f be Function of G1, G2 st the RingMorphismStr of G = RingMorphismStr (# G2, G3, g #) & the RingMorphismStr of F = RingMorphismStr (# G1, G2, f #) holds S1 = RingMorphismStr (# G1, G3, (g * f) #) and

         A13: for G1, G2, G3 holds for g be Function of G2, G3, f be Function of G1, G2 st the RingMorphismStr of G = RingMorphismStr (# G2, G3, g #) & the RingMorphismStr of F = RingMorphismStr (# G1, G2, f #) holds S2 = RingMorphismStr (# G1, G3, (g * f) #);

        consider G29,G39 be Ring such that

         A14: G29 <= G39 and

         A15: ( dom G) = G29 and ( cod G) = G39 and

         A16: the RingMorphismStr of G is Morphism of G29, G39 by Lm6;

        reconsider F9 as Morphism of G19, G29 by A1, A15, A10;

        consider f9 be Function of G19, G29 such that

         A17: F9 = RingMorphismStr (# G19, G29, f9 #) by A1, A15, A9;

        reconsider G9 = the RingMorphismStr of G as Morphism of G29, G39 by A16;

        consider g9 be Function of G29, G39 such that

         A18: G9 = RingMorphismStr (# G29, G39, g9 #) by A14, Lm8;



        thus S1 = RingMorphismStr (# G19, G39, (g9 * f9) #) by A12, A18, A17

        .= S2 by A13, A18, A17;

      end;

    end

    theorem :: RINGCAT1:5



     Th5: G1 <= G2 & G2 <= G3 implies G1 <= G3

    proof

      assume that

       A1: G1 <= G2 and

       A2: G2 <= G3;

      consider F0 be RingMorphism such that

       A3: ( dom F0) = G1 and

       A4: ( cod F0) = G2 by A1;

      reconsider F = the RingMorphismStr of F0 as RingMorphism by Lm2;

      ( dom F) = G1 & ( cod F) = G2 by A3, A4;

      then

      reconsider F9 = F as Morphism of G1, G2 by A1, Def8;

      consider f be Function of G1, G2 such that

       A5: F9 = RingMorphismStr (# G1, G2, f #) by A1, Lm8;

      consider G0 be RingMorphism such that

       A6: ( dom G0) = G2 and

       A7: ( cod G0) = G3 by A2;

      reconsider G = the RingMorphismStr of G0 as RingMorphism by Lm2;

      ( dom G) = G2 & ( cod G) = G3 by A6, A7;

      then

      reconsider G9 = G as Morphism of G2, G3 by A2, Def8;

      consider g be Function of G2, G3 such that

       A8: G9 = RingMorphismStr (# G2, G3, g #) by A2, Lm8;

      ( dom G) = ( cod F) by A4, A6;

      then (G * F) = RingMorphismStr (# G1, G3, (g * f) #) by A8, A5, Def9;

      then ( dom (G * F)) = G1 & ( cod (G * F)) = G3;

      hence thesis;

    end;

    theorem :: RINGCAT1:6



     Th6: for G be Morphism of G2, G3, F be Morphism of G1, G2 st G1 <= G2 & G2 <= G3 holds (G * F) is Morphism of G1, G3

    proof

      let G be Morphism of G2, G3, F be Morphism of G1, G2;

      assume that

       A1: G1 <= G2 and

       A2: G2 <= G3;

      consider g be Function of G2, G3 such that

       A3: G = RingMorphismStr (# G2, G3, g #) by A2, Lm8;

      consider f be Function of G1, G2 such that

       A4: F = RingMorphismStr (# G1, G2, f #) by A1, Lm8;

      ( dom G) = G2 by A2, Def8

      .= ( cod F) by A1, Def8;

      then (G * F) = RingMorphismStr (# G1, G3, (g * f) #) by A3, A4, Def9;

      then

       A5: ( dom (G * F)) = G1 & ( cod (G * F)) = G3;

      G1 <= G3 by A1, A2, Th5;

      hence thesis by A5, Def8;

    end;

    definition

      let G1, G2, G3;

      let G be Morphism of G2, G3, F be Morphism of G1, G2;

      assume

       A1: G1 <= G2 & G2 <= G3;

      :: RINGCAT1:def10

      func G *' F -> strict Morphism of G1, G3 equals

      : Def10: (G * F);

      coherence by A1, Th6;

    end

    theorem :: RINGCAT1:7



     Th7: for f,g be strict RingMorphism st ( dom g) = ( cod f) holds ex G1, G2, G3 st ex f0 be Function of G1, G2, g0 be Function of G2, G3 st f = RingMorphismStr (# G1, G2, f0 #) & g = RingMorphismStr (# G2, G3, g0 #) & (g * f) = RingMorphismStr (# G1, G3, (g0 * f0) #)

    proof

      let f,g be strict RingMorphism such that

       A1: ( dom g) = ( cod f);

      set G1 = ( dom f), G2 = ( cod f), G3 = ( cod g);

      reconsider g9 = g as Morphism of G2, G3 by A1, Th3;

      consider g0 be Function of G2, G3 such that

       A2: g9 = RingMorphismStr (# G2, G3, g0 #) by A1;

      reconsider f9 = f as Morphism of G1, G2 by Th3;

      consider f0 be Function of G1, G2 such that

       A3: f9 = RingMorphismStr (# G1, G2, f0 #);

      take G1, G2, G3, f0, g0;

      thus thesis by A1, A3, A2, Def9;

    end;

    theorem :: RINGCAT1:8



     Th8: for f,g be strict RingMorphism st ( dom g) = ( cod f) holds ( dom (g * f)) = ( dom f) & ( cod (g * f)) = ( cod g)

    proof

      let f,g be strict RingMorphism;

      assume ( dom g) = ( cod f);

      then

       A1: ex G1,G2,G3 be Ring, f0 be Function of G1, G2, g0 be Function of G2, G3 st f = RingMorphismStr (# G1, G2, f0 #) & g = RingMorphismStr (# G2, G3, g0 #) & (g * f) = RingMorphismStr (# G1, G3, (g0 * f0) #) by Th7;

      hence ( dom (g * f)) = ( dom f);

      thus thesis by A1;

    end;

    theorem :: RINGCAT1:9



     Th9: for f be Morphism of G1, G2, g be Morphism of G2, G3, h be Morphism of G3, G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds (h * (g * f)) = ((h * g) * f)

    proof

      let f be Morphism of G1, G2, g be Morphism of G2, G3, h be Morphism of G3, G4;

      assume that

       A1: G1 <= G2 and

       A2: G2 <= G3 and

       A3: G3 <= G4;

      consider f0 be Function of G1, G2 such that

       A4: f = RingMorphismStr (# G1, G2, f0 #) by A1, Lm8;

      consider h0 be Function of G3, G4 such that

       A5: h = RingMorphismStr (# G3, G4, h0 #) by A3, Lm8;

      consider g0 be Function of G2, G3 such that

       A6: g = RingMorphismStr (# G2, G3, g0 #) by A2, Lm8;



       A7: ( cod g) = G3 by A6;



       A8: ( dom h) = G3 by A5;

      then

       A9: (h * g) = RingMorphismStr (# G2, G4, (h0 * g0) #) by A6, A5, A7, Def9;



       A10: ( dom g) = G2 by A6;

      then

       A11: ( dom (h * g)) = G2 by A7, A8, Th8;



       A12: ( cod f) = G2 by A4;

      then

       A13: ( cod (g * f)) = G3 by A10, A7, Th8;

      (g * f) = RingMorphismStr (# G1, G3, (g0 * f0) #) by A4, A6, A12, A10, Def9;



      then (h * (g * f)) = RingMorphismStr (# G1, G4, (h0 * (g0 * f0)) #) by A5, A8, A13, Def9

      .= RingMorphismStr (# G1, G4, ((h0 * g0) * f0) #) by RELAT_1: 36

      .= ((h * g) * f) by A4, A12, A9, A11, Def9;

      hence thesis;

    end;

    theorem :: RINGCAT1:10



     Th10: for f,g,h be strict RingMorphism st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h * (g * f)) = ((h * g) * f)

    proof

      let f,g,h be strict RingMorphism such that

       A1: ( dom h) = ( cod g) and

       A2: ( dom g) = ( cod f);

      set G1 = ( dom f), G2 = ( cod f), G3 = ( cod g), G4 = ( cod h);

      reconsider h9 = h as Morphism of G3, G4 by A1, Th3;

      reconsider f9 = f as Morphism of G1, G2 by Th3;

      reconsider g9 = g as Morphism of G2, G3 by A2, Th3;



       A3: G1 <= G2;

      G2 <= G3 & G3 <= G4 by A1, A2;

      then (h9 * (g9 * f9)) = ((h9 * g9) * f9) by A3, Th9;

      hence thesis;

    end;

    theorem :: RINGCAT1:11

    ( dom ( ID G)) = G & ( cod ( ID G)) = G & (for f be strict RingMorphism st ( cod f) = G holds (( ID G) * f) = f) & for g be strict RingMorphism st ( dom g) = G holds (g * ( ID G)) = g

    proof

      set i = ( ID G);

      thus

       A1: ( dom i) = G & ( cod i) = G;

      thus for f be strict RingMorphism st ( cod f) = G holds (i * f) = f

      proof

        let f be strict RingMorphism such that

         A2: ( cod f) = G;

        set H = ( dom f);

        reconsider f9 = f as Morphism of H, G by A2, Th3;

        consider m be Function of H, G such that

         A3: f9 = RingMorphismStr (# H, G, m #) by A2;

        (( id G) * m) = m by FUNCT_2: 17;

        hence thesis by A1, A2, A3, Def9;

      end;

      thus for g be strict RingMorphism st ( dom g) = G holds (g * ( ID G)) = g

      proof

        let f be strict RingMorphism such that

         A4: ( dom f) = G;

        set H = ( cod f);

        reconsider f9 = f as Morphism of G, H by A4, Th3;

        consider m be Function of G, H such that

         A5: f9 = RingMorphismStr (# G, H, m #) by A4;

        (m * ( id G)) = m by FUNCT_2: 17;

        hence thesis by A1, A4, A5, Def9;

      end;

    end;

    definition

      let IT be set;

      :: RINGCAT1:def11

      attr IT is Ring_DOMAIN-like means

      : Def11: for x be Element of IT holds x is strict Ring;

    end

    registration

      cluster Ring_DOMAIN-like non empty for set;

      existence

      proof

        set X = the strict Ring;

        set D = {X};

        take D;

        for x be Element of D holds x is strict Ring by TARSKI:def 1;

        hence thesis;

      end;

    end

    definition

      mode Ring_DOMAIN is Ring_DOMAIN-like non empty set;

    end

    reserve V for Ring_DOMAIN;

    definition

      let V;

      :: original: Element

      redefine

      mode Element of V -> Ring ;

      coherence by Def11;

    end

    registration

      let V;

      cluster strict for Element of V;

      existence

      proof

        set e = the Element of V;

        e is strict Ring by Def11;

        hence thesis;

      end;

    end

    definition

      let IT be set;

      :: RINGCAT1:def12

      attr IT is RingMorphism_DOMAIN-like means

      : Def12: for x be object st x in IT holds x is strict RingMorphism;

    end

    registration

      cluster RingMorphism_DOMAIN-like for non empty set;

      existence

      proof

        set G = the Ring;

        take {( ID G)};

        for x be object st x in {( ID G)} holds x is strict RingMorphism by TARSKI:def 1;

        hence thesis;

      end;

    end

    definition

      mode RingMorphism_DOMAIN is RingMorphism_DOMAIN-like non empty set;

    end

    definition

      let M be RingMorphism_DOMAIN;

      :: original: Element

      redefine

      mode Element of M -> RingMorphism ;

      coherence by Def12;

    end

    registration

      let M be RingMorphism_DOMAIN;

      cluster strict for Element of M;

      existence

      proof

        set m = the Element of M;

        m is strict RingMorphism by Def12;

        hence thesis;

      end;

    end

    theorem :: RINGCAT1:12



     Th12: for f be strict RingMorphism holds {f} is RingMorphism_DOMAIN

    proof

      let f be strict RingMorphism;

      for x be object st x in {f} holds x is strict RingMorphism by TARSKI:def 1;

      hence thesis by Def12;

    end;

    definition

      let G, H;

      :: RINGCAT1:def13

      mode RingMorphism_DOMAIN of G,H -> RingMorphism_DOMAIN means

      : Def13: for x be Element of it holds x is Morphism of G, H;

      existence

      proof

        set F = the Morphism of G, H;

        reconsider D = {F} as RingMorphism_DOMAIN by Th12;

        take D;

        thus thesis by TARSKI:def 1;

      end;

    end

    theorem :: RINGCAT1:13



     Th13: D is RingMorphism_DOMAIN of G, H iff for x be Element of D holds x is Morphism of G, H

    proof

      thus D is RingMorphism_DOMAIN of G, H implies for x be Element of D holds x is Morphism of G, H by Def13;

      thus (for x be Element of D holds x is Morphism of G, H) implies D is RingMorphism_DOMAIN of G, H

      proof

        assume

         A1: for x be Element of D holds x is Morphism of G, H;

        then for x be object st x in D holds x is strict RingMorphism;

        then

        reconsider D9 = D as RingMorphism_DOMAIN by Def12;

        for x be Element of D9 holds x is Morphism of G, H by A1;

        hence thesis by Def13;

      end;

    end;

    theorem :: RINGCAT1:14

    for f be Morphism of G, H holds {f} is RingMorphism_DOMAIN of G, H

    proof

      let f be Morphism of G, H;

      for x be Element of {f} holds x is Morphism of G, H by TARSKI:def 1;

      hence thesis by Th13;

    end;

    definition

      let G, H;

      assume

       A1: G <= H;

      :: RINGCAT1:def14

      func Morphs (G,H) -> RingMorphism_DOMAIN of G, H means

      : Def14: for x be object holds x in it iff x is Morphism of G, H;

      existence

      proof

        set F = the Morphism of G, H;

        set D = { RingMorphismStr (# G, H, f #) where f be Element of ( Maps (G,H)) : f is linear };

        consider f be Function of G, H such that F = RingMorphismStr (# G, H, f #) and

         A2: f is linear by A1, Lm7;

        reconsider f0 = f as Element of ( Maps (G,H)) by FUNCT_2: 8;

         RingMorphismStr (# G, H, f0 #) in D by A2;

        then

        reconsider D as non empty set;



         A3: for x be object holds x in D implies x is Morphism of G, H

        proof

          let x be object;

          assume x in D;

          then ex f be Element of ( Maps (G,H)) st x = RingMorphismStr (# G, H, f #) & f is linear;

          hence thesis by Lm5;

        end;

        then

         A4: for x be Element of D holds x is Morphism of G, H;



         A5: for x be object holds x is Morphism of G, H implies x in D

        proof

          let x be object;

          assume x is Morphism of G, H;

          then

          reconsider x as Morphism of G, H;



           A6: ( dom x) = G & ( cod x) = H by A1, Def8;

          then

          reconsider f = the Fun of x as Function of G, H;

          reconsider g = f as Element of ( Maps (G,H)) by FUNCT_2: 8;



           A7: x = RingMorphismStr (# G, H, g #) by A6;

          the Fun of x is linear by Lm3;

          hence thesis by A7;

        end;

        reconsider D as RingMorphism_DOMAIN of G, H by A4, Th13;

        take D;

        thus thesis by A3, A5;

      end;

      uniqueness

      proof

        let D1,D2 be RingMorphism_DOMAIN of G, H such that

         A8: for x be object holds x in D1 iff x is Morphism of G, H and

         A9: for x be object holds x in D2 iff x is Morphism of G, H;

        for x be object holds x in D1 iff x in D2

        proof

          let x be object;

          hereby

            assume x in D1;

            then x is Morphism of G, H by A8;

            hence x in D2 by A9;

          end;

          assume x in D2;

          then x is Morphism of G, H by A9;

          hence thesis by A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let G, H;

      let M be RingMorphism_DOMAIN of G, H;

      :: original: Element

      redefine

      mode Element of M -> Morphism of G, H ;

      coherence by Def13;

    end

    registration

      let G, H;

      let M be RingMorphism_DOMAIN of G, H;

      cluster strict for Element of M;

      existence

      proof

        set e = the Element of M;

        e is Morphism of G, H;

        hence thesis;

      end;

    end

    definition

      let x,y be object;

      :: RINGCAT1:def15

      pred GO x,y means ex x1,x2,x3,x4,x5,x6 be set st x = [ [x1, x2, x3, x4], x5, x6] & ex G be strict Ring st y = G & x1 = the carrier of G & x2 = the addF of G & x3 = ( comp G) & x4 = ( 0. G) & x5 = the multF of G & x6 = ( 1. G);

    end

    theorem :: RINGCAT1:15



     Th15: for x,y1,y2 be object st GO (x,y1) & GO (x,y2) holds y1 = y2

    proof

      let x,y1,y2 be object such that

       A1: GO (x,y1) and

       A2: GO (x,y2);

      consider a1,a2,a3,a4,a5,a6 be set such that

       A3: x = [ [a1, a2, a3, a4], a5, a6] and

       A4: ex G be strict Ring st y1 = G & a1 = the carrier of G & a2 = the addF of G & a3 = ( comp G) & a4 = ( 0. G) & a5 = the multF of G & a6 = ( 1. G) by A1;

      consider b1,b2,b3,b4,b5,b6 be set such that

       A5: x = [ [b1, b2, b3, b4], b5, b6] and

       A6: ex G be strict Ring st y2 = G & b1 = the carrier of G & b2 = the addF of G & b3 = ( comp G) & b4 = ( 0. G) & b5 = the multF of G & b6 = ( 1. G) by A2;

      consider G2 be strict Ring such that

       A7: y2 = G2 and

       A8: b1 = the carrier of G2 & b2 = the addF of G2 and b3 = ( comp G2) and

       A9: b4 = ( 0. G2) and

       A10: b5 = the multF of G2 & b6 = ( 1. G2) by A6;

      consider G1 be strict Ring such that

       A11: y1 = G1 and

       A12: a1 = the carrier of G1 & a2 = the addF of G1 and a3 = ( comp G1) and

       A13: a4 = ( 0. G1) and

       A14: a5 = the multF of G1 & a6 = ( 1. G1) by A4;



       A15: the multF of G1 = the multF of G2 & ( 1. G1) = ( 1. G2) by A3, A5, A14, A10, XTUPLE_0: 3;



       A16: [a1, a2, a3, a4] = [b1, b2, b3, b4] by A3, A5, XTUPLE_0: 3;

      then the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 by A12, A8, XTUPLE_0: 5;

      hence thesis by A11, A13, A7, A9, A16, A15, XTUPLE_0: 5;

    end;

    theorem :: RINGCAT1:16



     Th16: ex x be object st x in UN & GO (x, Z_3 )

    proof

      set G = Z_3 ;

      reconsider x1 = the carrier of G, x2 = the addF of G, x3 = ( comp G), x4 = ( 0. G), x5 = the multF of G, x6 = ( 1. G) as Element of UN by MOD_2: 29;

      set x9 = [x1, x2, x3, x4];

      set x = [x9, x5, x6];

      take x;

      x9 is Element of UN by GRCAT_1: 1;

      hence thesis by GRCAT_1: 1;

    end;

    definition

      let UN;

      :: RINGCAT1:def16

      func RingObjects (UN) -> set means

      : Def16: for y be object holds y in it iff ex x st x in UN & GO (x,y);

      existence

      proof

        defpred P[ object, object] means GO ($1,$2);



         A1: for x,y1,y2 be object st P[x, y1] & P[x, y2] holds y1 = y2 by Th15;

        consider Y be set such that

         A2: for y be object holds y in Y iff ex x be object st x in UN & P[x, y] from TARSKI:sch 1( A1);

        take Y;

        let y be object;

        thus y in Y implies ex x st x in UN & GO (x,y)

        proof

          assume y in Y;

          then ex x be object st x in UN & P[x, y] by A2;

          hence thesis;

        end;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let Y1,Y2 be set such that

         A3: for y be object holds y in Y1 iff ex x st x in UN & GO (x,y) and

         A4: for y be object holds y in Y2 iff ex x st x in UN & GO (x,y);

        now

          let y be object;

          y in Y1 iff ex x st x in UN & GO (x,y) by A3;

          hence y in Y1 iff y in Y2 by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: RINGCAT1:17



     Th17: Z_3 in ( RingObjects UN)

    proof

      ex x be object st x in UN & GO (x, Z_3 ) by Th16;

      hence thesis by Def16;

    end;

    registration

      let UN;

      cluster ( RingObjects UN) -> non empty;

      coherence by Th17;

    end

    theorem :: RINGCAT1:18



     Th18: for x be Element of ( RingObjects UN) holds x is strict Ring

    proof

      let x be Element of ( RingObjects UN);

      consider u be set such that u in UN and

       A1: GO (u,x) by Def16;

      ex x1,x2,x3,x4,x5,x6 be set st u = [ [x1, x2, x3, x4], x5, x6] & ex G be strict Ring st x = G & x1 = the carrier of G & x2 = the addF of G & x3 = ( comp G) & x4 = ( 0. G) & x5 = the multF of G & x6 = ( 1. G) by A1;

      hence thesis;

    end;

    registration

      let UN;

      cluster ( RingObjects UN) -> Ring_DOMAIN-like;

      coherence by Th18;

    end

    definition

      let V;

      :: RINGCAT1:def17

      func Morphs (V) -> RingMorphism_DOMAIN means

      : Def17: for x be object holds x in it iff ex G,H be Element of V st G <= H & x is Morphism of G, H;

      existence

      proof

        set G0 = the Element of V;

        set M = ( Morphs (G0,G0)), S = { ( Morphs (G,H)) where G be Element of V, H be Element of V : G <= H };

        ( ID G0) is Element of M & M in S by Def14;

        then

        reconsider T = ( union S) as non empty set by TARSKI:def 4;



         A1: for x be object holds x in T iff ex G,H be Element of V st G <= H & x is Morphism of G, H

        proof

          let x be object;

          thus x in T implies ex G,H be Element of V st G <= H & x is Morphism of G, H

          proof

            assume x in T;

            then

            consider Y be set such that

             A2: x in Y and

             A3: Y in S by TARSKI:def 4;

            consider G,H be Element of V such that

             A4: Y = ( Morphs (G,H)) and

             A5: G <= H by A3;

            take G, H;

            x is Element of ( Morphs (G,H)) by A2, A4;

            hence thesis by A5;

          end;

          thus (ex G,H be Element of V st G <= H & x is Morphism of G, H) implies x in T

          proof

            given G,H be Element of V such that

             A6: G <= H & x is Morphism of G, H;

            set M = ( Morphs (G,H));

            x in M & M in S by A6, Def14;

            hence thesis by TARSKI:def 4;

          end;

        end;

        now

          let x be object;

          assume x in T;

          then ex G,H be Element of V st G <= H & x is Morphism of G, H by A1;

          hence x is strict RingMorphism;

        end;

        then

        reconsider T9 = T as RingMorphism_DOMAIN by Def12;

        take T9;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be RingMorphism_DOMAIN such that

         A7: for x be object holds x in D1 iff ex G,H be Element of V st G <= H & x is Morphism of G, H and

         A8: for x be object holds x in D2 iff ex G,H be Element of V st G <= H & x is Morphism of G, H;

        now

          let x be object;

          x in D1 iff ex G,H be Element of V st G <= H & x is Morphism of G, H by A7;

          hence x in D1 iff x in D2 by A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let V;

      let F be Element of ( Morphs V);

      :: original: dom

      redefine

      func dom (F) -> Element of V ;

      coherence

      proof

        consider G,H be Element of V such that

         A1: G <= H and

         A2: F is Morphism of G, H by Def17;

        reconsider F9 = F as Morphism of G, H by A2;

        ( dom F9) = G by A1, Def8;

        hence thesis;

      end;

      :: original: cod

      redefine

      func cod (F) -> Element of V ;

      coherence

      proof

        consider G,H be Element of V such that

         A3: G <= H and

         A4: F is Morphism of G, H by Def17;

        reconsider F9 = F as Morphism of G, H by A4;

        ( cod F9) = H by A3, Def8;

        hence thesis;

      end;

    end

    definition

      let V;

      let G be Element of V;

      :: RINGCAT1:def18

      func ID (G) -> strict Element of ( Morphs V) equals ( ID G);

      coherence by Def17;

      ::$Canceled

    end

    definition

      let V;

      :: RINGCAT1:def20

      func dom (V) -> Function of ( Morphs V), V means

      : Def19: for f be Element of ( Morphs V) holds (it . f) = ( dom f);

      existence

      proof

        deffunc G( Element of ( Morphs V)) = ( dom $1);

        consider F be Function of ( Morphs V), V such that

         A1: for f be Element of ( Morphs V) holds (F . f) = G(f) from FUNCT_2:sch 4;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Morphs V), V such that

         A2: for f be Element of ( Morphs V) holds (F1 . f) = ( dom f) and

         A3: for f be Element of ( Morphs V) holds (F2 . f) = ( dom f);

        now

          let f be Element of ( Morphs V);

          (F1 . f) = ( dom f) by A2;

          hence (F1 . f) = (F2 . f) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: RINGCAT1:def21

      func cod (V) -> Function of ( Morphs V), V means

      : Def20: for f be Element of ( Morphs V) holds (it . f) = ( cod f);

      existence

      proof

        deffunc G( Element of ( Morphs V)) = ( cod $1);

        consider F be Function of ( Morphs V), V such that

         A4: for f be Element of ( Morphs V) holds (F . f) = G(f) from FUNCT_2:sch 4;

        take F;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Morphs V), V such that

         A5: for f be Element of ( Morphs V) holds (F1 . f) = ( cod f) and

         A6: for f be Element of ( Morphs V) holds (F2 . f) = ( cod f);

        now

          let f be Element of ( Morphs V);

          (F1 . f) = ( cod f) by A5;

          hence (F1 . f) = (F2 . f) by A6;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      ::$Canceled

    end

    theorem :: RINGCAT1:19



     Th19: for g,f be Element of ( Morphs V) st ( dom g) = ( cod f) holds ex G1,G2,G3 be Element of V st G1 <= G2 & G2 <= G3 & g is Morphism of G2, G3 & f is Morphism of G1, G2

    proof

      set X = ( Morphs V);

      defpred P[ Element of X, Element of X] means ( dom $1) = ( cod $2);

      let g,f be Element of X such that

       A1: P[g, f];

      consider G2,G3 be Element of V such that

       A2: G2 <= G3 & g is Morphism of G2, G3 by Def17;

      consider G1,G29 be Element of V such that

       A3: G1 <= G29 & f is Morphism of G1, G29 by Def17;



       A4: G29 = ( cod f) by A3, Def8;

      G2 = ( dom g) by A2, Def8;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: RINGCAT1:20



     Th20: for g,f be Element of ( Morphs V) st ( dom g) = ( cod f) holds (g * f) in ( Morphs V)

    proof

      set X = ( Morphs V);

      defpred P[ Element of X, Element of X] means ( dom $1) = ( cod $2);

      let g,f be Element of X;

      assume P[g, f];

      then

      consider G1,G2,G3 be Element of V such that

       A1: G1 <= G2 & G2 <= G3 and

       A2: g is Morphism of G2, G3 and

       A3: f is Morphism of G1, G2 by Th19;

      reconsider f9 = f as Morphism of G1, G2 by A3;

      reconsider g9 = g as Morphism of G2, G3 by A2;

      G1 <= G3 & (g9 *' f9) = (g9 * f9) by A1, Def10, Th5;

      hence thesis by Def17;

    end;

    definition

      let V;

      :: RINGCAT1:def23

      func comp (V) -> PartFunc of [:( Morphs V), ( Morphs V):], ( Morphs V) means

      : Def21: (for g,f be Element of ( Morphs V) holds [g, f] in ( dom it ) iff ( dom g) = ( cod f)) & for g,f be Element of ( Morphs V) st [g, f] in ( dom it ) holds (it . (g,f)) = (g * f);

      existence

      proof

        set X = ( Morphs V);

        defpred P[ Element of X, Element of X] means ( dom $1) = ( cod $2);

        deffunc F( Element of X, Element of X) = ($1 * $2);



         A1: for g,f be Element of X st P[g, f] holds F(g,f) in X by Th20;

        consider c be PartFunc of [:X, X:], X such that

         A2: (for g,f be Element of X holds [g, f] in ( dom c) iff P[g, f]) & for g,f be Element of X st [g, f] in ( dom c) holds (c . (g,f)) = F(g,f) from BINOP_1:sch 8( A1);

        take c;

        thus thesis by A2;

      end;

      uniqueness

      proof

        set X = ( Morphs V);

        defpred P[ Element of X, Element of X] means ( dom $1) = ( cod $2);

        let c1,c2 be PartFunc of [:X, X:], X such that

         A3: for g,f be Element of X holds [g, f] in ( dom c1) iff P[g, f] and

         A4: for g,f be Element of X st [g, f] in ( dom c1) holds (c1 . (g,f)) = (g * f) and

         A5: for g,f be Element of X holds [g, f] in ( dom c2) iff P[g, f] and

         A6: for g,f be Element of X st [g, f] in ( dom c2) holds (c2 . (g,f)) = (g * f);

        set V0 = ( dom c1);

         A7:

        now

          let x be object;

          assume

           A8: x in ( dom c1);

          then

          consider g,f be Element of X such that

           A9: x = [g, f] by SUBSET_1: 43;

           P[g, f] by A3, A8, A9;

          hence x in ( dom c2) by A5, A9;

        end;

        then

         A10: ( dom c1) c= ( dom c2) by TARSKI:def 3;



         A11: for x,y be object st [x, y] in V0 holds (c1 . (x,y)) = (c2 . (x,y))

        proof

          let x,y be object;

          assume

           A12: [x, y] in V0;

          then

          reconsider x, y as Element of X by ZFMISC_1: 87;

          (c1 . (x,y)) = (x * y) by A4, A12;

          hence thesis by A6, A7, A12;

        end;

        now

          let x be object;

          assume

           A13: x in ( dom c2);

          then

          consider g,f be Element of X such that

           A14: x = [g, f] by SUBSET_1: 43;

           P[g, f] by A5, A13, A14;

          hence x in ( dom c1) by A3, A14;

        end;

        then ( dom c2) c= ( dom c1) by TARSKI:def 3;

        hence thesis by A11, A10, BINOP_1: 20, XBOOLE_0:def 10;

      end;

    end

    definition

      let UN;

      :: RINGCAT1:def24

      func RingCat (UN) -> CatStr equals CatStr (# ( RingObjects UN), ( Morphs ( RingObjects UN)), ( dom ( RingObjects UN)), ( cod ( RingObjects UN)), ( comp ( RingObjects UN)) #);

      coherence ;

    end

    registration

      let UN;

      cluster ( RingCat UN) -> strict non void non empty;

      coherence ;

    end

    theorem :: RINGCAT1:21



     Th21: for f,g be Morphism of ( RingCat UN) holds [g, f] in ( dom the Comp of ( RingCat UN)) iff ( dom g) = ( cod f)

    proof

      set C = ( RingCat UN), V = ( RingObjects UN);

      let f,g be Morphism of C;

      reconsider f9 = f as Element of ( Morphs V);

      reconsider g9 = g as Element of ( Morphs V);

      ( dom g) = ( dom g9) & ( cod f) = ( cod f9) by Def19, Def20;

      hence thesis by Def21;

    end;

    theorem :: RINGCAT1:22



     Th22: for f be Morphism of ( RingCat UN), f9 be Element of ( Morphs ( RingObjects UN)), b be Object of ( RingCat UN), b9 be Element of ( RingObjects UN) holds f is strict Element of ( Morphs ( RingObjects UN)) & f9 is Morphism of ( RingCat UN) & b is strict Element of ( RingObjects UN) & b9 is Object of ( RingCat UN)

    proof

      set C = ( RingCat UN), V = ( RingObjects UN);

      set X = ( Morphs V);

      let f be Morphism of C, f9 be Element of X, b be Object of C, b9 be Element of V;

      consider x such that x in UN and

       A1: GO (x,b) by Def16;

      ex G,H be Element of V st G <= H & f is Morphism of G, H by Def17;

      hence f is strict Element of X;

      thus f9 is Morphism of C;

      ex x1,x2,x3,x4,x5,x6 be set st x = [ [x1, x2, x3, x4], x5, x6] & ex G be strict Ring st b = G & x1 = the carrier of G & x2 = the addF of G & x3 = ( comp G) & x4 = ( 0. G) & x5 = the multF of G & x6 = ( 1. G) by A1;

      hence b is strict Element of V;

      thus thesis;

    end;

    ::$Canceled

    theorem :: RINGCAT1:24



     Th23: for f,g be Morphism of ( RingCat UN), f9,g9 be Element of ( Morphs ( RingObjects UN)) st f = f9 & g = g9 holds (( dom g) = ( cod f) iff ( dom g9) = ( cod f9)) & (( dom g) = ( cod f) iff [g9, f9] in ( dom ( comp ( RingObjects UN)))) & (( dom g) = ( cod f) implies (g (*) f) = (g9 * f9)) & (( dom f) = ( dom g) iff ( dom f9) = ( dom g9)) & (( cod f) = ( cod g) iff ( cod f9) = ( cod g9))

    proof

      set C = ( RingCat UN), V = ( RingObjects UN);

      set X = ( Morphs V);

      let f,g be Morphism of C;

      let f9,g9 be Element of X;

      assume that

       A1: f = f9 and

       A2: g = g9;



       A3: ( cod f) = ( cod f9) by A1, Def20;

      hence ( dom g) = ( cod f) iff ( dom g9) = ( cod f9) by A2, Def19;

      ( dom g) = ( dom g9) by A2, Def19;

      hence

       A4: ( dom g) = ( cod f) iff [g9, f9] in ( dom ( comp V)) by A3, Def21;

      thus ( dom g) = ( cod f) implies (g (*) f) = (g9 * f9)

      proof

        assume

         A5: ( dom g) = ( cod f);

        then [g, f] in ( dom the Comp of C) by Th21;



        hence (g (*) f) = (( comp V) . (g9,f9)) by A1, A2, CAT_1:def 1

        .= (g9 * f9) by A4, A5, Def21;

      end;

      ( dom f) = ( dom f9) by A1, Def19;

      hence ( dom f) = ( dom g) iff ( dom f9) = ( dom g9) by A2, Def19;

      ( cod g) = ( cod g9) by A2, Def20;

      hence thesis by A1, Def20;

    end;



     Lm9: for f,g be Morphism of ( RingCat UN) st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g)

    proof

      set X = ( Morphs ( RingObjects UN));

      let f,g be Morphism of ( RingCat UN) such that

       A1: ( dom g) = ( cod f);

      reconsider g9 = g as strict Element of X by Th22;

      reconsider f9 = f as strict Element of X by Th22;



       A2: ( dom g9) = ( cod f9) by A1, Th23;

      then

      reconsider gf = (g9 * f9) as Element of X by Th20;



       A3: gf = (g (*) f) by A1, Th23;

      ( dom (g9 * f9)) = ( dom f9) & ( cod (g9 * f9)) = ( cod g9) by A2, Th8;

      hence thesis by A3, Th23;

    end;



     Lm10: for f,g,h be Morphism of ( RingCat UN) st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

    proof

      set X = ( Morphs ( RingObjects UN));

      let f,g,h be Morphism of ( RingCat UN) such that

       A1: ( dom h) = ( cod g) & ( dom g) = ( cod f);

      reconsider f9 = f, g9 = g, h9 = h as strict Element of X by Th22;



       A2: (h9 * g9) = (h (*) g) & ( dom (h (*) g)) = ( cod f) by A1, Lm9, Th23;



       A3: ( dom h9) = ( cod g9) & ( dom g9) = ( cod f9) by A1, Th23;

      then

      reconsider gf = (g9 * f9), hg = (h9 * g9) as strict Element of X by Th20;

      (g9 * f9) = (g (*) f) & ( dom h) = ( cod (g (*) f)) by A1, Lm9, Th23;



      then (h (*) (g (*) f)) = (h9 * gf) by Th23

      .= (hg * f9) by A3, Th10

      .= ((h (*) g) (*) f) by A2, Th23;

      hence thesis;

    end;

    registration

      let UN;

      cluster ( RingCat UN) -> Category-like transitive associative reflexive;

      coherence

      proof

        set C = ( RingCat UN);

        thus C is Category-like by Th21;

        thus C is transitive by Lm9;

        thus C is associative by Lm10;

        thus C is reflexive

        proof

          let a be Element of C;

          reconsider G = a as Element of ( RingObjects UN);

          consider x such that x in UN and

           A1: GO (x,G) by Def16;

          set ii = ( ID G);

          consider x1,x2,x3,x4,x5,x6 be set such that x = [ [x1, x2, x3, x4], x5, x6] and

           A2: ex H be strict Ring st G = H & x1 = the carrier of H & x2 = the addF of H & x3 = ( comp H) & x4 = ( 0. H) & x5 = the multF of H & x6 = ( 1. H) by A1;

          reconsider G as strict Element of ( RingObjects UN) by A2;

          reconsider ii as Morphism of C;

          reconsider ia = ii as RingMorphismStr;



           A3: ( dom ii) = ( dom ia) by Def19

          .= a;

          ( cod ii) = ( cod ia) by Def20

          .= a;

          then ii in ( Hom (a,a)) by A3;

          hence ( Hom (a,a)) <> {} ;

        end;

      end;

    end



     Lm11: for a be Element of ( RingCat UN), aa be Element of ( RingObjects UN) st a = aa holds for i be Morphism of a, a st i = ( ID aa) holds for b be Element of ( RingCat UN) holds (( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) i) = g) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (i (*) f) = f)

    proof

      let a be Element of ( RingCat UN), aa be Element of ( RingObjects UN) such that a = aa;

      let i be Morphism of a, a such that

       A1: i = ( ID aa);

      let b be Element of ( RingCat UN);

      thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) i) = g

      proof

        assume

         A2: ( Hom (a,b)) <> {} ;

        let g be Morphism of a, b;

        reconsider gg = g, ii = i as Element of ( Morphs ( RingObjects UN));

        consider G1,H1 be Element of ( RingObjects UN) such that

         A3: G1 <= H1 and

         A4: gg is Morphism of G1, H1 by Def17;

        consider f be Function of G1, H1 such that

         A5: gg = RingMorphismStr (# G1, H1, f #) by A3, A4, Lm8;



         A6: ( Hom (a,a)) <> {} by CAT_1:def 9;



         A7: ( dom g) = a by A2, CAT_1: 5

        .= ( cod i) by A6, CAT_1: 5;

        then

         A8: ( dom gg) = ( cod ii) by Th23;

        then

        reconsider f as Function of aa, H1 by A5, A1;



         A9: [gg, ii] in ( dom ( comp ( RingObjects UN))) by Th23, A7;



        hence (g (*) i) = (( comp ( RingObjects UN)) . (g,i)) by CAT_1:def 1

        .= (gg * ii) by A9, Def21

        .= RingMorphismStr (# aa, H1, (f * ( id aa)) #) by A1, Def9, A5, A8

        .= g by A1, A5, A8, FUNCT_2: 17;

      end;

      thus ( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (i (*) f) = f

      proof

        assume

         A10: ( Hom (b,a)) <> {} ;

        let g be Morphism of b, a;

        reconsider gg = g, ii = i as Element of ( Morphs ( RingObjects UN));

        consider G1,H1 be Element of ( RingObjects UN) such that

         A11: G1 <= H1 and

         A12: gg is Morphism of G1, H1 by Def17;

        consider f be Function of G1, H1 such that

         A13: gg = RingMorphismStr (# G1, H1, f #) by A11, A12, Lm8;



         A14: ( Hom (a,a)) <> {} by CAT_1:def 9;



         A15: ( cod g) = a by A10, CAT_1: 5

        .= ( dom i) by A14, CAT_1: 5;

        then

         A16: ( cod gg) = ( dom ii) by Th23;

        reconsider f as Function of G1, aa by A13, A1, A16;



         A17: [ii, gg] in ( dom ( comp ( RingObjects UN))) by A15, Th23;



        hence (i (*) g) = (( comp ( RingObjects UN)) . (i,g)) by CAT_1:def 1

        .= (ii * gg) by A17, Def21

        .= RingMorphismStr (# G1, aa, (( id aa) * f) #) by A1, Def9, A13, A16

        .= g by A1, A16, A13, FUNCT_2: 17;

      end;

    end;

    registration

      let UN;

      cluster ( RingCat UN) -> with_identities;

      coherence

      proof

        set C = ( RingCat UN);

        let a be Element of C;

        reconsider aa = a as Element of ( RingObjects UN);

        reconsider ii = ( ID aa) as Morphism of C;

        reconsider ia = ii as RingMorphismStr;



         A1: ( dom ii) = ( dom ia) by Def19

        .= a;

        ( cod ii) = ( cod ia) by Def20

        .= a;

        then

        reconsider ii as Morphism of a, a by A1, CAT_1: 4;

        take ii;

        thus thesis by Lm11;

      end;

    end

    theorem :: RINGCAT1:25

    for a be Object of ( RingCat UN), aa be Element of ( RingObjects UN) st a = aa holds ( id a) = ( ID aa)

    proof

      let a be Object of ( RingCat UN), aa be Element of ( RingObjects UN);

      set C = ( RingCat UN);

      assume

       A1: a = aa;

      reconsider ii = ( ID aa) as Morphism of C;

      reconsider ia = ii as RingMorphismStr;



       A2: ( dom ii) = ( dom ia) by Def19

      .= a by A1;

      ( cod ii) = ( cod ia) by Def20

      .= a by A1;

      then

      reconsider ii as Morphism of a, a by A2, CAT_1: 4;

      for b be Object of C holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) ii) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (ii (*) f) = f) by A1, Lm11;

      hence ( id a) = ( ID aa) by CAT_1:def 12;

    end;