modcat_1.miz

    begin

    reserve x,y for set;

    reserve D for non empty set;

    reserve UN for Universe;

    reserve R for Ring;

    reserve G,H for LeftMod of R;

    definition

      let R;

      :: MODCAT_1:def1

      mode LeftMod_DOMAIN of R -> non empty set means

      : Def1: for x be Element of it holds x is strict LeftMod of R;

      existence

      proof

        set D = {( TrivialLMod R)};

        take D;

        thus thesis by TARSKI:def 1;

      end;

    end

    reserve V for LeftMod_DOMAIN of R;

    definition

      let R, V;

      :: original: Element

      redefine

      mode Element of V -> LeftMod of R ;

      coherence by Def1;

    end

    registration

      let R, V;

      cluster strict for Element of V;

      existence

      proof

        set e = the Element of V;

        take e;

        thus thesis by Def1;

      end;

    end

    definition

      let R;

      :: MODCAT_1:def2

      mode LModMorphism_DOMAIN of R -> non empty set means

      : Def2: for x be Element of it holds x is strict LModMorphism of R;

      existence

      proof

        set G = the LeftMod of R;

        take {( ID G)};

        let x be Element of {( ID G)};

        thus thesis by TARSKI:def 1;

      end;

    end

    definition

      let R;

      let M be LModMorphism_DOMAIN of R;

      :: original: Element

      redefine

      mode Element of M -> LModMorphism of R ;

      coherence by Def2;

    end

    registration

      let R;

      let M be LModMorphism_DOMAIN of R;

      cluster strict for Element of M;

      existence

      proof

        set e = the Element of M;

        take e;

        thus thesis by Def2;

      end;

    end

    theorem :: MODCAT_1:1



     Th1: for f be strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R

    proof

      let f be strict LModMorphism of R;

      for x be Element of {f} holds x is strict LModMorphism of R by TARSKI:def 1;

      hence thesis by Def2;

    end;

    definition

      let R, G, H;

      :: MODCAT_1:def3

      mode LModMorphism_DOMAIN of G,H -> LModMorphism_DOMAIN of R means

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

      existence

      proof

        reconsider D = {( ZERO (G,H))} as LModMorphism_DOMAIN of R by Th1;

        take D;

        thus thesis by TARSKI:def 1;

      end;

    end

    theorem :: MODCAT_1:2



     Th2: D is LModMorphism_DOMAIN of G, H iff for x be Element of D holds x is strict Morphism of G, H

    proof

      thus D is LModMorphism_DOMAIN of G, H implies for x be Element of D holds x is strict Morphism of G, H by Def3;

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

      proof

        assume

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

        then for x be Element of D holds x is strict LModMorphism of R;

        then

        reconsider D9 = D as LModMorphism_DOMAIN of R by Def2;

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

        hence thesis by Def3;

      end;

    end;

    theorem :: MODCAT_1:3

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

    proof

      let f be strict Morphism of G, H;

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

      hence thesis by Th2;

    end;

    definition

      let R, G, H;

      :: MODCAT_1:def4

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

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

      existence

      proof

        ( ZeroMap (G,H)) is Element of ( Funcs (the carrier of G,the carrier of H)) by FUNCT_2: 8;

        then

        reconsider f0 = ( ZeroMap (G,H)) as Element of ( Maps (G,H)) by GRCAT_1:def 21;

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

         LModMorphismStr (# G, H, f0 #) in D;

        then

        reconsider D as non empty set;



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

        proof

          let x be object;

          assume x is strict Morphism of G, H;

          then

          reconsider x as strict Morphism of G, H;

          ( dom x) = G by MOD_2:def 8;

          then

           A2: the Dom of x = G;



           A3: ( cod x) = H by MOD_2:def 8;

          then the Cod of x = H;

          then

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

          f is Element of ( Funcs (the carrier of G,the carrier of H)) by FUNCT_2: 8;

          then

          reconsider g = f as Element of ( Maps (G,H)) by GRCAT_1:def 21;

          the Fun of x is additive homogeneous & x = LModMorphismStr (# G, H, g #) by A3, A2, MOD_2: 4;

          hence thesis;

        end;



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

        proof

          let x be object;

          assume x in D;

          then ex f be Element of ( Maps (G,H)) st x = LModMorphismStr (# G, H, f #) & f is additive homogeneous;

          hence thesis by MOD_2: 6;

        end;

        then for x be Element of D holds x is strict Morphism of G, H;

        then

        reconsider D as LModMorphism_DOMAIN of G, H by Th2;

        take D;

        thus thesis by A4, A1;

      end;

      uniqueness

      proof

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

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

         A6: for x be object holds x in D2 iff x is strict 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 strict Morphism of G, H by A5;

            hence x in D2 by A6;

          end;

          assume x in D2;

          then x is strict Morphism of G, H by A6;

          hence thesis by A5;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let R, G, H;

      let M be LModMorphism_DOMAIN of G, H;

      :: original: Element

      redefine

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

      coherence by Def3;

    end

    definition

      let x,y be object;

      let R;

      :: MODCAT_1:def5

      pred GO x,y,R means ex x1,x2 be object st x = [x1, x2] & ex G be strict LeftMod of R st y = G & x1 = the addLoopStr of G & x2 = the lmult of G;

    end

    theorem :: MODCAT_1:4



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

    proof

      let x,y1,y2 be object such that

       A1: GO (x,y1,R) and

       A2: GO (x,y2,R);

      consider a1,a2 be object such that

       A3: x = [a1, a2] and

       A4: ex G be strict LeftMod of R st y1 = G & a1 = the addLoopStr of G & a2 = the lmult of G by A1;

      consider G1 be strict LeftMod of R such that

       A5: y1 = G1 and

       A6: a1 = the addLoopStr of G1 and

       A7: a2 = the lmult of G1 by A4;

      consider b1,b2 be object such that

       A8: x = [b1, b2] and

       A9: ex G be strict LeftMod of R st y2 = G & b1 = the addLoopStr of G & b2 = the lmult of G by A2;

      consider G2 be strict LeftMod of R such that

       A10: y2 = G2 and

       A11: b1 = the addLoopStr of G2 and

       A12: b2 = the lmult of G2 by A9;

       the addLoopStr of G1 = the addLoopStr of G2 by A3, A8, A6, A11, XTUPLE_0: 1;

      hence thesis by A3, A8, A5, A7, A10, A12, XTUPLE_0: 1;

    end;

    theorem :: MODCAT_1:5

    for UN holds ex x be object st x in the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, { {} }:], { {} })) & GO (x,( TrivialLMod R),R)

    proof

      let UN;

      set T = ( TrivialLMod R);

      reconsider x1 = the addLoopStr of T as Element of ( GroupObjects UN) by GRCAT_1: 29;

      reconsider f1 = the lmult of T as Function of [:the carrier of R, { {} }:], { {} };

      reconsider x2 = f1 as Element of ( Funcs ( [:the carrier of R, { {} }:], { {} })) by FUNCT_2: 8;

      take x = [x1, x2];

      thus x in the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, { {} }:], { {} }));

      thus thesis;

    end;

    definition

      let UN, R;

      :: MODCAT_1:def6

      func LModObjects (UN,R) -> set means

      : Def6: for y be object holds y in it iff ex x st x in the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, the carrier of G:],the carrier of G)) & GO (x,y,R);

      existence

      proof

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

        set N = the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, the carrier of G:],the carrier of G));



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

        consider Y be set such that

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

        take Y;

        let y be object;

        thus y in Y implies ex x st x in the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, the carrier of G:],the carrier of G)) & GO (x,y,R)

        proof

          assume y in Y;

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

          hence thesis;

        end;

        thus thesis by A2;

      end;

      uniqueness

      proof

        set N = the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, the carrier of G:],the carrier of G));

        let Y1,Y2 be set such that

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

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

        now

          let y be object;

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

          hence y in Y1 iff y in Y2 by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: MODCAT_1:6



     Th6: ( TrivialLMod R) in ( LModObjects (UN,R))

    proof

      set G0 = Trivial-addLoopStr , f0 = ( pr2 (the carrier of R, { 0 }));

      reconsider G0 as Element of ( GroupObjects UN) by GRCAT_1: 29;

      reconsider f0 as Element of ( Funcs ( [:the carrier of R, the carrier of G0:],the carrier of G0)) by FUNCT_2: 8;

      set x = [G0, f0];



       A1: x in the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, the carrier of G:],the carrier of G));

       GO (x,( TrivialLMod R),R);

      hence thesis by A1, Def6;

    end;

    registration

      let UN, R;

      cluster ( LModObjects (UN,R)) -> non empty;

      coherence by Th6;

    end

    theorem :: MODCAT_1:7



     Th7: for x be Element of ( LModObjects (UN,R)) holds x is strict LeftMod of R

    proof

      let x be Element of ( LModObjects (UN,R));

      set N = the set of all [G, f] where G be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, the carrier of G:],the carrier of G));

      consider u be set such that u in N and

       A1: GO (u,x,R) by Def6;

      ex a1,a2 be object st u = [a1, a2] & ex G be strict LeftMod of R st x = G & a1 = the addLoopStr of G & a2 = the lmult of G by A1;

      hence thesis;

    end;

    definition

      let UN, R;

      :: original: LModObjects

      redefine

      func LModObjects (UN,R) -> LeftMod_DOMAIN of R ;

      coherence

      proof

        for x be Element of ( LModObjects (UN,R)) holds x is strict LeftMod of R by Th7;

        hence thesis by Def1;

      end;

    end

    definition

      let R, V;

      :: MODCAT_1:def7

      func Morphs (V) -> LModMorphism_DOMAIN of R means

      : Def7: for x be object holds x in it iff ex G,H be strict Element of V st x is strict Morphism of G, H;

      existence

      proof

        set G0 = the strict Element of V;

        set M = ( Morphs (G0,G0)), S = the set of all ( Morphs (G,H)) where G be strict Element of V, H be strict Element of V;

        ( ZERO (G0,G0)) is Element of M & M in S by Def4;

        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 strict Element of V st x is strict Morphism of G, H

        proof

          let x be object;

          thus x in T implies ex G,H be strict Element of V st x is strict 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 strict Element of V such that

             A4: Y = ( Morphs (G,H)) by A3;

            take G, H;

            thus thesis by A2, A4, Def4;

          end;

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

          proof

            given G,H be strict Element of V such that

             A5: x is strict Morphism of G, H;

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



             A6: M in S;

            x in M by A5, Def4;

            hence thesis by A6, TARSKI:def 4;

          end;

        end;

        now

          let x be Element of T;

          ex G,H be strict Element of V st x is strict Morphism of G, H by A1;

          hence x is strict LModMorphism of R;

        end;

        then

        reconsider T9 = T as LModMorphism_DOMAIN of R by Def2;

        take T9;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be LModMorphism_DOMAIN of R such that

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

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

        now

          let x be object;

          x in D1 iff ex G,H be strict Element of V st x is strict 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 R, V;

      let F be Element of ( Morphs V);

      :: MODCAT_1:def8

      func dom' (F) -> Element of V equals ( dom F);

      coherence

      proof

        consider G,H be strict Element of V such that

         A1: F is strict Morphism of G, H by Def7;

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

        ( dom F9) = G by MOD_2:def 8;

        hence thesis;

      end;

      :: MODCAT_1:def9

      func cod' (F) -> Element of V equals ( cod F);

      coherence

      proof

        consider G,H be strict Element of V such that

         A2: F is strict Morphism of G, H by Def7;

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

        ( cod F9) = H by MOD_2:def 8;

        hence thesis;

      end;

    end

    definition

      let R, V;

      let G be Element of V;

      :: MODCAT_1:def10

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

      coherence

      proof

        reconsider G as strict Element of V by Def1;

        ( ID G) is strict Element of ( Morphs V) by Def7;

        hence thesis;

      end;

    end

    definition

      let R, V;

      :: MODCAT_1:def11

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

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

      :: MODCAT_1:def12

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

      : Def12: 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 :: MODCAT_1:8



     Th8: for g,f be Element of ( Morphs V) st ( dom' g) = ( cod' f) holds ex G1,G2,G3 be strict Element of V st 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 strict Element of V such that

       A2: g is strict Morphism of G2, G3 by Def7;

      consider G1,G29 be strict Element of V such that

       A3: f is strict Morphism of G1, G29 by Def7;



       A4: G29 = ( cod' f) by A3, MOD_2:def 8;

      G2 = ( dom' g) by A2, MOD_2:def 8;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: MODCAT_1:9



     Th9: 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 strict Element of V such that

       A1: g is Morphism of G2, G3 and

       A2: f is Morphism of G1, G2 by Th8;

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

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

      (g9 * f9) = (g9 *' f9);

      hence thesis by Def7;

    end;

    theorem :: MODCAT_1:10



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

    proof

      let g,f be Element of ( Morphs V);

      assume ( dom g) = ( cod f);

      then ( dom' g) = ( cod' f);

      hence thesis by Th9;

    end;

    definition

      let R, V;

      :: MODCAT_1:def14

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

      : Def13: (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 Th9;

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

        now

          let x be object;

          assume

           A7: x in ( dom c1);

          then

          consider g,f be Element of X such that

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

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

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

        end;

        then

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



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

        proof

          let x,y be object;

          assume

           A11: [x, y] in V0;

          then

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

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

          hence thesis by A6, A9, A11;

        end;

        now

          let x be object;

          assume

           A12: x in ( dom c2);

          then

          consider g,f be Element of X such that

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

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

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

        end;

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

        then ( dom c1) = ( dom c2) by A9, XBOOLE_0:def 10;

        hence thesis by A10, BINOP_1: 20;

      end;

    end

    theorem :: MODCAT_1:11



     Th11: for g,f be Element of ( Morphs V) holds [g, f] in ( dom ( comp V)) iff ( dom g) = ( cod f)

    proof

      let g,f be Element of ( Morphs V);

      ( dom g) = ( dom' g) & ( cod f) = ( cod' f);

      hence thesis by Def13;

    end;

    definition

      let UN, R;

      :: MODCAT_1:def15

      func LModCat (UN,R) -> strict CatStr equals CatStr (# ( LModObjects (UN,R)), ( Morphs ( LModObjects (UN,R))), ( dom ( LModObjects (UN,R))), ( cod ( LModObjects (UN,R))), ( comp ( LModObjects (UN,R))) #);

      coherence ;

    end

    registration

      let UN, R;

      cluster ( LModCat (UN,R)) -> non void non empty;

      coherence ;

    end

    theorem :: MODCAT_1:12



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

    proof

      set C = ( LModCat (UN,R)), V = ( LModObjects (UN,R));

      let f,g be Morphism of C;

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

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



       A1: ( cod f) = ( cod' f9) by Def12

      .= ( cod f9);



       A2: ( dom g) = ( dom' g9) by Def11

      .= ( dom g9);

       A3:

      now

        assume ( dom g) = ( cod f);

        then ( dom' g9) = ( cod' f9) by A2, A1;

        hence [g, f] in ( dom the Comp of C) by Def13;

      end;

      now

        assume [g, f] in ( dom the Comp of C);



        then ( dom' g9) = ( cod' f9) by Def13

        .= ( cod f9);

        hence ( dom g) = ( cod f) by A2, A1;

      end;

      hence thesis by A3;

    end;

    registration

      let UN, R;

      cluster -> strict for Element of ( Morphs ( LModObjects (UN,R)));

      coherence

      proof

        set V = ( LModObjects (UN,R));

        let f be Element of ( Morphs V);

        ex G,H be strict Element of V st f is strict Morphism of G, H by Def7;

        hence f is strict;

      end;

    end

    ::$Canceled

    theorem :: MODCAT_1:15



     Th13: for f be Morphism of ( LModCat (UN,R)) holds for f9 be Element of ( Morphs ( LModObjects (UN,R))) st f = f9 holds ( dom f) = ( dom f9) & ( cod f) = ( cod f9)

    proof

      set C = ( LModCat (UN,R)), V = ( LModObjects (UN,R));

      set X = ( Morphs V);

      let f be Morphism of C, f9 be Element of X;

      assume

       A1: f = f9;



      hence ( dom f) = ( dom' f9) by Def11

      .= ( dom f9);



      thus ( cod f) = ( cod' f9) by A1, Def12

      .= ( cod f9);

    end;

    theorem :: MODCAT_1:16



     Th14: for f,g be Morphism of ( LModCat (UN,R)), f9,g9 be Element of ( Morphs ( LModObjects (UN,R))) 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 ( LModObjects (UN,R))))) & (( 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 = ( LModCat (UN,R)), V = ( LModObjects (UN,R));

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

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

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

      hence

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

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



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

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

      end;

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

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

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

      hence thesis by A1, Th13;

    end;



     Lm1: for f,g be Morphism of ( LModCat (UN,R)) st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g)

    proof

      set X = ( Morphs ( LModObjects (UN,R)));

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

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

      reconsider g9 = g as strict Element of X;

      reconsider f9 = f as strict Element of X;



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

      then

       A3: ( dom (g9 * f9)) = ( dom f9) & ( cod (g9 * f9)) = ( cod g9) by MOD_2: 15;

      reconsider gf = (g9 * f9) as Element of X by A2, Th10;

      gf = (g (*) f) by A1, Th14;

      hence thesis by A3, Th14;

    end;



     Lm2: for f,g,h be Morphism of ( LModCat (UN,R)) st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

    proof

      set X = ( Morphs ( LModObjects (UN,R)));

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

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

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



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



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

      then

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

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



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

      .= (hg * f9) by A3, MOD_2: 17

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

      hence thesis;

    end;

    registration

      let UN, R;

      cluster ( LModCat (UN,R)) -> Category-like transitive associative reflexive;

      coherence

      proof

        set C = ( LModCat (UN,R));

        thus C is Category-like by Th14;

        thus C is transitive by Lm1;

        thus C is associative by Lm2;

        thus C is reflexive

        proof

          let a be Element of C;

          reconsider G = a as Element of ( LModObjects (UN,R));

          consider x such that x in the set of all [H, f] where H be Element of ( GroupObjects UN), f be Element of ( Funcs ( [:the carrier of R, the carrier of H:],the carrier of H)) and

           A1: GO (x,G,R) by Def6;

          set ii = ( ID G);

          consider x1,x2 be object such that x = [x1, x2] and

           A2: ex H be strict LeftMod of R st G = H & x1 = the addLoopStr of H & x2 = the lmult of H by A1;

          reconsider G as strict Element of ( LModObjects (UN,R)) by A2;

          reconsider ii as Morphism of C;

          reconsider ia = ii as LModMorphismStr over R;



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

          .= a;

          ( cod ii) = ( cod ia) by Th13

          .= a;

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

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

        end;

      end;

    end