grcat_1.miz

    begin

    reserve x,y for set;

    reserve D for non empty set;

    reserve UN for Universe;

    theorem :: GRCAT_1:1



     Th1: for u1,u2,u3,u4 be Element of UN holds [u1, u2, u3] in UN & [u1, u2, u3, u4] in UN

    proof

      let u1,u2,u3,u4 be Element of UN;

       [u1, u2, u3] = [ [u1, u2], u3] & [u1, u2, u3, u4] = [ [u1, u2, u3], u4];

      hence thesis by CLASSES2: 58;

    end;

    theorem :: GRCAT_1:2



     Th2: ( op2 . ( {} , {} )) = {} & ( op1 . {} ) = {} & op0 = {}

    proof

       [ {} , {} ] in [: { {} }, { {} }:] by ZFMISC_1: 28;

      hence ( op2 . ( {} , {} )) = {} by FUNCT_2: 50;

       {} in { {} } by TARSKI:def 1;

      hence ( op1 . {} ) = {} by FUNCT_2: 50;

      thus thesis;

    end;

    theorem :: GRCAT_1:3



     Th3: { {} } in UN & [ { {} }, { {} }] in UN & [: { {} }, { {} }:] in UN & op2 in UN & op1 in UN

    proof

      set D = { {} };

      thus

       A1: D in UN by CLASSES2: 56, CLASSES2: 57;

      hence [D, D] in UN by CLASSES2: 58;



       A2: op2 in ( Funcs ( [:D, D:],D)) by FUNCT_2: 8;

      thus [:D, D:] in UN by A1, CLASSES2: 61;

      then ( Funcs ( [:D, D:],D)) in UN by A1, CLASSES2: 61;

      hence op2 in UN by A2, ORDINAL1: 10;



       A3: op1 in ( Funcs (D,D)) by FUNCT_2: 8;

      ( Funcs (D,D)) in UN by A1, CLASSES2: 61;

      hence thesis by A3, ORDINAL1: 10;

    end;

    registration

      cluster Trivial-addLoopStr -> midpoint_operator;

      coherence

      proof

        set G = Trivial-addLoopStr ;



         A1: for a be Element of G holds ex x be Element of G st ( Double x) = a

        proof

          set x = the Element of G;

          let a be Element of G;

          take x;



          thus ( Double x) = {} by TARSKI:def 1

          .= a by TARSKI:def 1;

        end;

        for a be Element of G st ( Double a) = ( 0. G) holds a = ( 0. G) by TARSKI:def 1;

        hence thesis by A1, MIDSP_2:def 5;

      end;

    end

    theorem :: GRCAT_1:4

    (for x be Element of Trivial-addLoopStr holds x = {} ) & (for x,y be Element of Trivial-addLoopStr holds (x + y) = {} ) & (for x be Element of Trivial-addLoopStr holds ( - x) = {} ) & ( 0. Trivial-addLoopStr ) = {} by TARSKI:def 1;

    reserve C for Category;

    reserve O for non empty Subset of the carrier of C;

    definition

      let C, O;

      :: GRCAT_1:def1

      func Morphs (O) -> Subset of the carrier' of C equals ( union { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O });

      coherence by CAT_2: 19;

    end

    registration

      let C, O;

      cluster ( Morphs O) -> non empty;

      coherence by CAT_2: 19;

    end

    definition

      let C, O;

      :: GRCAT_1:def2

      func dom (O) -> Function of ( Morphs O), O equals (the Source of C | ( Morphs O));

      coherence by CAT_2: 20;

      :: GRCAT_1:def3

      func cod (O) -> Function of ( Morphs O), O equals (the Target of C | ( Morphs O));

      coherence by CAT_2: 20;

      :: GRCAT_1:def4

      func comp (O) -> PartFunc of [:( Morphs O), ( Morphs O):], ( Morphs O) equals (the Comp of C || ( Morphs O));

      coherence by CAT_2: 20;

      ::$Canceled

    end

    definition

      let C, O;

      :: GRCAT_1:def6

      func cat (O) -> Subcategory of C equals CatStr (# O, ( Morphs O), ( dom O), ( cod O), ( comp O) #);

      coherence by CAT_2: 21;

    end

    registration

      let C, O;

      cluster ( cat O) -> strict;

      coherence ;

    end

    theorem :: GRCAT_1:5

    the carrier of ( cat O) = O;

    definition

      let G be non empty 1-sorted, H be non empty ZeroStr;

      :: GRCAT_1:def7

      func ZeroMap (G,H) -> Function of G, H equals (the carrier of G --> ( 0. H));

      coherence ;

    end

    theorem :: GRCAT_1:6



     Th6: ( comp Trivial-addLoopStr ) = op1

    proof

      reconsider f = ( comp Trivial-addLoopStr ) as Function of { {} }, { {} };

      for x be object st x in { {} } holds ( op1 . x) = (f . x)

      proof

        let x be object;

        assume x in { {} };

        then

        reconsider x as Element of Trivial-addLoopStr ;

        x = {} by TARSKI:def 1;



        then ( op1 . x) = ( - x) by Th2, TARSKI:def 1

        .= (f . x) by VECTSP_1:def 13;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    registration

      let G be non empty addMagma, H be right_zeroed non empty addLoopStr;

      cluster ( ZeroMap (G,H)) -> additive;

      coherence

      proof

        set f = ( ZeroMap (G,H));

        let x,y be Element of G;



         A1: (f . y) = ( 0. H) by FUNCOP_1: 7;

        (f . (x + y)) = ( 0. H) & (f . x) = ( 0. H) by FUNCOP_1: 7;

        hence thesis by A1, RLVECT_1:def 4;

      end;

    end

    registration

      let G be non empty addMagma, H be right_zeroed non empty addLoopStr;

      cluster additive for Function of G, H;

      existence

      proof

        take ( ZeroMap (G,H));

        thus thesis;

      end;

    end

    theorem :: GRCAT_1:7



     Th7: for G1,G2,G3 be non empty addMagma, f be Function of G1, G2, g be Function of G2, G3 st f is additive & g is additive holds (g * f) is additive

    proof

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

       A1: f is additive and

       A2: g is additive;

      set h = (g * f);

      now

        let x,y be Element 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;

      hence thesis;

    end;

    registration

      let G1 be non empty addMagma, G2,G3 be right_zeroed non empty addLoopStr, f be additive Function of G1, G2, g be additive Function of G2, G3;

      cluster (g * f) -> additive;

      coherence by Th7;

    end

    reserve G,H for AddGroup;

    definition

      struct GroupMorphismStr (# the Source, Target -> AddGroup,

the Fun -> Function of the Source, the Target #)

       attr strict strict;

    end

    definition

      ::$Canceled

      let f be GroupMorphismStr;

      :: GRCAT_1:def9

      func dom (f) -> AddGroup equals the Source of f;

      coherence ;

      :: GRCAT_1:def10

      func cod (f) -> AddGroup equals the Target of f;

      coherence ;

    end

    definition

      let f be GroupMorphismStr;

      :: GRCAT_1:def11

      func fun (f) -> Function of ( dom f), ( cod f) equals the Fun of f;

      coherence ;

    end

    theorem :: GRCAT_1:8

    for f be GroupMorphismStr, G1,G2 be AddGroup, f0 be Function of G1, G2 st f = GroupMorphismStr (# G1, G2, f0 #) holds ( dom f) = G1 & ( cod f) = G2 & ( fun f) = f0;

    definition

      let G, H;

      :: GRCAT_1:def12

      func ZERO (G,H) -> GroupMorphismStr equals GroupMorphismStr (# G, H, ( ZeroMap (G,H)) #);

      coherence ;

    end

    registration

      let G, H;

      cluster ( ZERO (G,H)) -> strict;

      coherence ;

    end

    definition

      let IT be GroupMorphismStr;

      :: GRCAT_1:def13

      attr IT is GroupMorphism-like means

      : Def11: ( fun IT) is additive;

    end

    registration

      cluster strict GroupMorphism-like for GroupMorphismStr;

      existence

      proof

        set G = the AddGroup;

        set z = ( ZERO (G,G));

        z is GroupMorphism-like;

        hence thesis;

      end;

    end

    definition

      mode GroupMorphism is GroupMorphism-like GroupMorphismStr;

    end

    theorem :: GRCAT_1:9



     Th9: for F be GroupMorphism holds the Fun of F is additive

    proof

      let F be GroupMorphism;

      the Fun of F = ( fun F);

      hence thesis by Def11;

    end;

    registration

      let G, H;

      cluster ( ZERO (G,H)) -> GroupMorphism-like;

      coherence ;

    end

    definition

      let G, H;

      :: GRCAT_1:def14

      mode Morphism of G,H -> GroupMorphism means

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

      existence

      proof

        take ( ZERO (G,H));

        thus thesis;

      end;

    end

    registration

      let G, H;

      cluster strict for Morphism of G, H;

      existence

      proof

        ( dom ( ZERO (G,H))) = G & ( cod ( ZERO (G,H))) = H;

        then ( ZERO (G,H)) is Morphism of G, H by Def12;

        hence thesis;

      end;

    end

    theorem :: GRCAT_1:10



     Th10: for f be strict GroupMorphismStr st ( dom f) = G & ( cod f) = H & ( fun f) is additive holds f is strict Morphism of G, H

    proof

      let f be strict GroupMorphismStr;

      assume that

       A1: ( dom f) = G & ( cod f) = H and

       A2: ( fun f) is additive;

      reconsider f9 = f as strict GroupMorphism by A2, Def11;

      f9 is strict Morphism of G, H by A1, Def12;

      hence thesis;

    end;

    theorem :: GRCAT_1:11



     Th11: for f be Function of G, H st f is additive holds GroupMorphismStr (# G, H, f #) is strict Morphism of G, H

    proof

      let f be Function of G, H such that

       A1: f is additive;

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

      ( fun F) = f;

      hence thesis by A1, Th10;

    end;

    registration

      let G be non empty addMagma;

      cluster ( id G) -> additive;

      coherence

      proof

        set f = ( id G);

        let x,y be Element of G;

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

        hence thesis by FUNCT_1: 18;

      end;

    end

    definition

      let G;

      :: GRCAT_1:def15

      func ID G -> Morphism of G, G equals GroupMorphismStr (# G, G, ( id G) #);

      coherence

      proof

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

        ( fun i) = ( id G);

        hence thesis by Th10;

      end;

    end

    registration

      let G;

      cluster ( ID G) -> strict;

      coherence ;

    end

    definition

      let G, H;

      :: original: ZERO

      redefine

      func ZERO (G,H) -> strict Morphism of G, H ;

      coherence

      proof

        set i = ( ZERO (G,H));

        ( fun i) = ( ZeroMap (G,H));

        hence thesis by Th10;

      end;

    end

    theorem :: GRCAT_1:12



     Th12: for F be Morphism of G, H holds ex f be Function of G, H st the GroupMorphismStr of F = GroupMorphismStr (# G, H, f #) & f is additive

    proof

      let F be Morphism of G, H;



       A1: the Target of F = ( cod F)

      .= H by Def12;



       A2: the Source of F = ( dom F)

      .= G by Def12;

      then

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

      take f;

      thus thesis by A2, A1, Th9;

    end;

    theorem :: GRCAT_1:13



     Th13: for F be strict Morphism of G, H holds ex f be Function of G, H st F = GroupMorphismStr (# G, H, f #)

    proof

      let F be strict Morphism of G, H;

      consider f be Function of G, H such that

       A1: F = GroupMorphismStr (# G, H, f #) and f is additive by Th12;

      take f;

      thus thesis by A1;

    end;

    theorem :: GRCAT_1:14



     Th14: for F be GroupMorphism holds ex G, H st F is Morphism of G, H

    proof

      let F be GroupMorphism;

      take G = the Source of F, H = the Target of F;

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

      hence thesis by Def12;

    end;

    theorem :: GRCAT_1:15

    for F be strict GroupMorphism holds ex G,H be AddGroup, f be Function of G, H st F is Morphism of G, H & F = GroupMorphismStr (# G, H, f #) & f is additive

    proof

      let F be strict GroupMorphism;

      consider G, H such that

       A1: F is Morphism of G, H by Th14;

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

      consider f be Function of G, H such that

       A2: F9 = GroupMorphismStr (# G, H, f #) & f is additive by Th12;

      take G, H, f;

      thus thesis by A2;

    end;

    theorem :: GRCAT_1:16



     Th16: for g,f be GroupMorphism st ( dom g) = ( cod f) holds ex G1,G2,G3 be AddGroup st g is Morphism of G2, G3 & f is Morphism of G1, G2

    proof

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

      let g,f be GroupMorphism such that

       A1: P[g, f];

      consider G2,G3 be AddGroup such that

       A2: g is Morphism of G2, G3 by Th14;

      consider G1,G29 be AddGroup such that

       A3: f is Morphism of G1, G29 by Th14;



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

      G2 = ( dom g) by A2, Def12;

      hence thesis by A1, A2, A3, A4;

    end;

    definition

      let G,F be GroupMorphism;

      assume

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

      :: GRCAT_1:def16

      func G * F -> strict GroupMorphism means

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

      existence

      proof

        consider G19,G29,G39 be AddGroup such that

         A2: G is Morphism of G29, G39 and

         A3: F is Morphism of G19, G29 by A1, Th16;

        consider f9 be Function of G19, G29 such that

         A4: the GroupMorphismStr of F = GroupMorphismStr (# G19, G29, f9 #) and

         A5: f9 is additive by A3, Th12;

        consider g9 be Function of G29, G39 such that

         A6: the GroupMorphismStr of G = GroupMorphismStr (# G29, G39, g9 #) and

         A7: g9 is additive by A2, Th12;

        (g9 * f9) is additive by A7, A5;

        then

        reconsider T9 = GroupMorphismStr (# G19, G39, (g9 * f9) #) as strict GroupMorphism by Th11;

        take T9;

        thus thesis by A6, A4;

      end;

      uniqueness

      proof

        consider G19,G299 be AddGroup such that

         A8: F is Morphism of G19, G299 by Th14;

        reconsider F9 = F as Morphism of G19, G299 by A8;

        consider G29,G39 be AddGroup such that

         A9: G is Morphism of G29, G39 by Th14;

        G29 = ( dom G) by A9, Def12;

        then

        reconsider F9 as Morphism of G19, G29 by A1, Def12;

        consider f9 be Function of G19, G29 such that

         A10: the GroupMorphismStr of F9 = GroupMorphismStr (# G19, G29, f9 #) and f9 is additive by Th12;

        reconsider G9 = G as Morphism of G29, G39 by A9;

        let S1,S2 be strict GroupMorphism such that

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

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

        consider g9 be Function of G29, G39 such that

         A13: the GroupMorphismStr of G9 = GroupMorphismStr (# G29, G39, g9 #) and g9 is additive by Th12;



        thus S1 = GroupMorphismStr (# G19, G39, (g9 * f9) #) by A11, A13, A10

        .= S2 by A12, A13, A10;

      end;

    end

    theorem :: GRCAT_1:17



     Th17: for G1,G2,G3 be AddGroup, G be Morphism of G2, G3, F be Morphism of G1, G2 holds (G * F) is Morphism of G1, G3

    proof

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

      consider g be Function of G2, G3 such that

       A1: the GroupMorphismStr of G = GroupMorphismStr (# G2, G3, g #) and g is additive by Th12;

      consider f be Function of G1, G2 such that

       A2: the GroupMorphismStr of F = GroupMorphismStr (# G1, G2, f #) and f is additive by Th12;

      ( dom G) = G2 by Def12

      .= ( cod F) by Def12;

      then (G * F) = GroupMorphismStr (# G1, G3, (g * f) #) by A1, A2, Def14;

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

      hence thesis by Def12;

    end;

    definition

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

      :: original: *

      redefine

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

      coherence by Th17;

    end

    theorem :: GRCAT_1:18



     Th18: for G1,G2,G3 be AddGroup, G be Morphism of G2, G3, F be Morphism of G1, G2, g be Function of G2, G3, f be Function of G1, G2 st G = GroupMorphismStr (# G2, G3, g #) & F = GroupMorphismStr (# G1, G2, f #) holds (G * F) = GroupMorphismStr (# G1, G3, (g * f) #)

    proof

      let G1,G2,G3 be AddGroup, G be Morphism of G2, G3, F be Morphism of G1, G2, g be Function of G2, G3, f be Function of G1, G2 such that

       A1: G = GroupMorphismStr (# G2, G3, g #) & F = GroupMorphismStr (# G1, G2, f #);

      ( dom G) = G2 by Def12

      .= ( cod F) by Def12;

      hence thesis by A1, Def14;

    end;

    theorem :: GRCAT_1:19



     Th19: for f,g be strict GroupMorphism st ( dom g) = ( cod f) holds ex G1,G2,G3 be AddGroup, f0 be Function of G1, G2, g0 be Function of G2, G3 st f = GroupMorphismStr (# G1, G2, f0 #) & g = GroupMorphismStr (# G2, G3, g0 #) & (g * f) = GroupMorphismStr (# G1, G3, (g0 * f0) #)

    proof

      let f,g be strict GroupMorphism such that

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

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

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

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

      consider f0 be Function of G1, G2 such that

       A2: f9 = GroupMorphismStr (# G1, G2, f0 #);

      consider g0 be Function of G2, G3 such that

       A3: g9 = GroupMorphismStr (# G2, G3, g0 #) by Th13;

      take G1, G2, G3, f0, g0;

      thus thesis by A2, A3, Th18;

    end;

    theorem :: GRCAT_1:20



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

    proof

      let f,g be strict GroupMorphism;

      assume ( dom g) = ( cod f);

      then

       A1: ex G1,G2,G3 be AddGroup, f0 be Function of G1, G2, g0 be Function of G2, G3 st f = GroupMorphismStr (# G1, G2, f0 #) & g = GroupMorphismStr (# G2, G3, g0 #) & (g * f) = GroupMorphismStr (# G1, G3, (g0 * f0) #) by Th19;

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

      thus thesis by A1;

    end;

    theorem :: GRCAT_1:21



     Th21: for G1,G2,G3,G4 be AddGroup, f be strict Morphism of G1, G2, g be strict Morphism of G2, G3, h be strict Morphism of G3, G4 holds (h * (g * f)) = ((h * g) * f)

    proof

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

      consider f0 be Function of G1, G2 such that

       A1: f = GroupMorphismStr (# G1, G2, f0 #) by Th13;

      consider g0 be Function of G2, G3 such that

       A2: g = GroupMorphismStr (# G2, G3, g0 #) by Th13;

      consider h0 be Function of G3, G4 such that

       A3: h = GroupMorphismStr (# G3, G4, h0 #) by Th13;



       A4: (h * g) = GroupMorphismStr (# G2, G4, (h0 * g0) #) by A2, A3, Th18;

      (g * f) = GroupMorphismStr (# G1, G3, (g0 * f0) #) by A1, A2, Th18;



      then (h * (g * f)) = GroupMorphismStr (# G1, G4, (h0 * (g0 * f0)) #) by A3, Th18

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

      .= ((h * g) * f) by A1, A4, Th18;

      hence thesis;

    end;

    theorem :: GRCAT_1:22



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

    proof

      let f,g,h be strict GroupMorphism such that

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

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

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

      reconsider h9 = h as Morphism of G3, ( cod h) by A1, Def12;

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

      reconsider f9 = f as Morphism of ( dom f), G2 by Def12;

      (h9 * (g9 * f9)) = ((h9 * g9) * f9) by Th21;

      hence thesis;

    end;

    theorem :: GRCAT_1:23

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

    proof

      set i = ( ID G);

      thus ( dom i) = G;

      thus ( cod i) = G;

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

      proof

        let f be strict GroupMorphism such that

         A1: ( cod f) = G;

        set H = ( dom f);

        reconsider f9 = f as Morphism of H, G by A1, Def12;

        consider m be Function of H, G such that

         A2: f9 = GroupMorphismStr (# H, G, m #) by Th13;

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

        hence thesis by A1, A2, Def14;

      end;

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

      proof

        let f be strict GroupMorphism such that

         A3: ( dom f) = G;

        set H = ( cod f);

        reconsider f9 = f as Morphism of G, H by A3, Def12;

        consider m be Function of G, H such that

         A4: f9 = GroupMorphismStr (# G, H, m #) by Th13;

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

        hence thesis by A3, A4, Def14;

      end;

    end;

    definition

      let IT be set;

      :: GRCAT_1:def17

      attr IT is Group_DOMAIN-like means

      : Def15: for x be object st x in IT holds x is strict AddGroup;

    end

    registration

      cluster Group_DOMAIN-like non empty for set;

      existence

      proof

        set D = { Trivial-addLoopStr };

        take D;

        for x be object st x in D holds x is strict AddGroup by TARSKI:def 1;

        hence thesis;

      end;

    end

    definition

      mode Group_DOMAIN is Group_DOMAIN-like non empty set;

    end

    reserve V for Group_DOMAIN;

    definition

      let V;

      :: original: Element

      redefine

      mode Element of V -> AddGroup ;

      coherence by Def15;

    end

    registration

      let V;

      cluster strict for Element of V;

      existence

      proof

        set v = the Element of V;

        v is strict AddGroup by Def15;

        hence thesis;

      end;

    end

    definition

      let IT be set;

      :: GRCAT_1:def18

      attr IT is GroupMorphism_DOMAIN-like means

      : Def16: for x be object st x in IT holds x is strict GroupMorphism;

    end

    registration

      cluster GroupMorphism_DOMAIN-like non empty for set;

      existence

      proof

        set G = the AddGroup;

        take {( ID G)};

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

        hence thesis;

      end;

    end

    definition

      mode GroupMorphism_DOMAIN is GroupMorphism_DOMAIN-like non empty set;

    end

    definition

      let M be GroupMorphism_DOMAIN;

      :: original: Element

      redefine

      mode Element of M -> GroupMorphism ;

      coherence by Def16;

    end

    registration

      let M be GroupMorphism_DOMAIN;

      cluster strict for Element of M;

      existence

      proof

        set m = the Element of M;

        m is strict GroupMorphism by Def16;

        hence thesis;

      end;

    end

    theorem :: GRCAT_1:24



     Th24: for f be strict GroupMorphism holds {f} is GroupMorphism_DOMAIN

    proof

      let f be strict GroupMorphism;

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

      hence thesis by Def16;

    end;

    definition

      let G, H;

      :: GRCAT_1:def19

      mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means

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

      existence

      proof

        reconsider D = {( ZERO (G,H))} as GroupMorphism_DOMAIN by Th24;

        take D;

        thus thesis by TARSKI:def 1;

      end;

    end

    theorem :: GRCAT_1:25



     Th25: D is GroupMorphism_DOMAIN of G, H iff for x be Element of D holds x is strict Morphism of G, H

    proof

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

      thus (for x be Element of D holds x is strict Morphism of G, H) implies D is GroupMorphism_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 object st x in D holds x is strict GroupMorphism;

        then

        reconsider D9 = D as GroupMorphism_DOMAIN by Def16;

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

        hence thesis by Def17;

      end;

    end;

    theorem :: GRCAT_1:26

    for f be strict Morphism of G, H holds {f} is GroupMorphism_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 Th25;

    end;

    definition

      let G,H be 1-sorted;

      :: GRCAT_1:def20

      mode MapsSet of G,H -> set means

      : Def18: for x be set st x in it holds x is Function of G, H;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    definition

      let G,H be 1-sorted;

      :: GRCAT_1:def21

      func Maps (G,H) -> MapsSet of G, H equals ( Funcs (the carrier of G,the carrier of H));

      coherence

      proof

        let x be set;

        assume x in ( Funcs (the carrier of G,the carrier of H));

        hence thesis by FUNCT_2: 66;

      end;

    end

    registration

      let G be 1-sorted, H be non empty 1-sorted;

      cluster ( Maps (G,H)) -> non empty;

      coherence ;

    end

    registration

      let G be 1-sorted, H be non empty 1-sorted;

      cluster non empty for MapsSet of G, H;

      existence

      proof

        ( Maps (G,H)) is non empty;

        hence thesis;

      end;

    end

    definition

      let G be 1-sorted, H be non empty 1-sorted;

      let M be non empty MapsSet of G, H;

      :: original: Element

      redefine

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

      coherence by Def18;

    end

    definition

      let G, H;

      :: GRCAT_1:def22

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

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

      existence

      proof

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

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

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

        then

        reconsider D as non empty set;



         A1: 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 = GroupMorphismStr (# G, H, f #) & f is additive;

          hence thesis by Th11;

        end;

        then

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



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



           A4: ( dom x) = G & ( cod x) = H by Def12;

          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;



           A5: x = GroupMorphismStr (# G, H, g #) by A4;

          the Fun of x is additive by Th9;

          hence thesis by A5;

        end;

        reconsider D as GroupMorphism_DOMAIN of G, H by A2, Th25;

        take D;

        thus thesis by A1, A3;

      end;

      uniqueness

      proof

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

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

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

          thus x in D1 implies x in D2

          proof

            assume x in D1;

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

            hence thesis by A7;

          end;

          thus x in D2 implies x in D1

          proof

            assume x in D2;

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

            hence thesis by A6;

          end;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let G, H;

      let M be GroupMorphism_DOMAIN of G, H;

      :: original: Element

      redefine

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

      coherence by Def17;

    end

    registration

      let G, H;

      let M be GroupMorphism_DOMAIN of G, H;

      cluster strict for Element of M;

      existence

      proof

        set m = the Element of M;

        m is strict Morphism of G, H by Def17;

        hence thesis;

      end;

    end

    definition

      let x,y be object;

      :: GRCAT_1:def23

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

    end

    theorem :: GRCAT_1:27



     Th27: 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 be set such that

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

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

      consider G1 be strict AddGroup such that

       A5: y1 = G1 and

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

       A7: a4 = ( 0. G1) by A4;

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

       A8: x = [b1, b2, b3, b4] and

       A9: ex G be strict AddGroup st y2 = G & b1 = the carrier of G & b2 = the addF of G & b3 = ( comp G) & b4 = ( 0. G) by A2;

      consider G2 be strict AddGroup such that

       A10: y2 = G2 and

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

       A12: b4 = ( 0. G2) by A9;

      the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2 by A3, A8, A6, A11, XTUPLE_0: 5;

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

    end;

    theorem :: GRCAT_1:28



     Th28: ex x st x in UN & GO (x, Trivial-addLoopStr )

    proof

      reconsider x2 = op2 as Element of UN by Th3;

      reconsider x3 = ( comp Trivial-addLoopStr ) as Element of UN by Th3, Th6;

      reconsider u = {} as Element of UN by CLASSES2: 56;

      set x1 = {u};

      ( Extract {} ) = u;

      then

      reconsider x4 = ( Extract {} ) as Element of UN;

      reconsider x = [x1, x2, x3, x4] as set by TARSKI: 1;

      take x;

      thus x in UN by Th1;

      take x1, x2, x3, x4;

      thus x = [x1, x2, x3, x4];

      take Trivial-addLoopStr ;

      thus thesis;

    end;

    definition

      let UN;

      :: GRCAT_1:def24

      func GroupObjects (UN) -> set means

      : Def22: for y be object holds y in it iff ex x be object 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 Th27;

        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 be object st x in UN & GO (x,y) by A2;

        thus thesis by A2;

      end;

      uniqueness

      proof

        defpred P[ object] means ex x be object st x in UN & GO (x,$1);

        for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

        hence thesis;

      end;

    end

    theorem :: GRCAT_1:29



     Th29: Trivial-addLoopStr in ( GroupObjects UN)

    proof

      ex x st x in UN & GO (x, Trivial-addLoopStr ) by Th28;

      hence thesis by Def22;

    end;

    registration

      let UN;

      cluster ( GroupObjects UN) -> non empty;

      coherence by Th29;

    end

    theorem :: GRCAT_1:30



     Th30: for x be Element of ( GroupObjects UN) holds x is strict AddGroup

    proof

      let x be Element of ( GroupObjects UN);

      consider u be object such that u in UN and

       A1: GO (u,x) by Def22;

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

      hence thesis;

    end;

    registration

      let UN;

      cluster ( GroupObjects UN) -> Group_DOMAIN-like;

      coherence by Th30;

    end

    definition

      let V;

      :: GRCAT_1:def25

      func Morphs (V) -> GroupMorphism_DOMAIN means

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

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

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

            hence thesis by A6, TARSKI:def 4;

          end;

        end;

        now

          let x be object;

          assume x in T;

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

          hence x is strict GroupMorphism;

        end;

        then

        reconsider T9 = T as GroupMorphism_DOMAIN by Def16;

        take T9;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be GroupMorphism_DOMAIN 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 V;

      let F be Element of ( Morphs V);

      :: original: dom

      redefine

      func dom (F) -> strict Element of V ;

      coherence

      proof

        consider G,H be strict Element of V such that

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

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

        ( dom F9) = G by Def12;

        hence thesis;

      end;

      :: original: cod

      redefine

      func cod (F) -> strict Element of V ;

      coherence

      proof

        consider G,H be strict Element of V such that

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

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

        ( cod F9) = H by Def12;

        hence thesis;

      end;

    end

    definition

      let V;

      let G be Element of V;

      :: GRCAT_1:def26

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

      coherence

      proof

        reconsider G9 = G as strict Element of V by Def15;

        ( ID G9) is strict Element of ( Morphs V) by Def23;

        hence thesis;

      end;

    end

    definition

      let V;

      :: GRCAT_1:def27

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

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

      existence

      proof

        deffunc F( 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) = F(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;

      :: GRCAT_1:def28

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

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

      existence

      proof

        deffunc F( 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) = F(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;

    end

    theorem :: GRCAT_1:31



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

      consider G1,G29 be strict Element of V such that

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



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

      G2 = ( dom g) by A2, Def12;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: GRCAT_1:32



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

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

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

      (g9 * f9) is Morphism of G1, G3;

      hence thesis by Def23;

    end;

    definition

      let V;

      :: GRCAT_1:def29

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

      : Def27: (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 Th32;

        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 V9 = ( dom c1);



         A7: ( dom c1) c= [:X, X:] by RELAT_1:def 18;

        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 A7, 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 V9 holds (c1 . (x,y)) = (c2 . (x,y))

        proof

          let x,y be object;

          assume

           A12: [x, y] in V9;

          then

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

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

          hence thesis by A6, A10, A12;

        end;

        now

          let x be object;

          assume

           A13: x in ( dom c2);

          ( dom c2) c= [:X, X:] by RELAT_1:def 18;

          then

          consider g,f be Element of X such that

           A14: x = [g, f] by A13, 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;

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

        hence thesis by A11, BINOP_1: 20;

      end;

    end

    definition

      let UN;

      :: GRCAT_1:def30

      func GroupCat (UN) -> non empty non void strict CatStr equals CatStr (# ( GroupObjects UN), ( Morphs ( GroupObjects UN)), ( dom ( GroupObjects UN)), ( cod ( GroupObjects UN)), ( comp ( GroupObjects UN)) #);

      coherence ;

    end

    registration

      let UN;

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

      coherence ;

    end

    theorem :: GRCAT_1:33



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

    proof

      set C = ( GroupCat UN), V = ( GroupObjects 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 Def25, Def26;

      hence thesis by Def27;

    end;

    theorem :: GRCAT_1:34



     Th34: for f be Morphism of ( GroupCat UN), f9 be Element of ( Morphs ( GroupObjects UN)), b be Object of ( GroupCat UN), b9 be Element of ( GroupObjects UN) holds f is strict Element of ( Morphs ( GroupObjects UN)) & f9 is Morphism of ( GroupCat UN) & b is strict Element of ( GroupObjects UN) & b9 is Object of ( GroupCat UN)

    proof

      set C = ( GroupCat UN), V = ( GroupObjects 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 be object such that x in UN and

       A1: GO (x,b) by Def22;

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

      hence f is strict Element of X;

      thus f9 is Morphism of C;

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

      hence b is strict Element of V;

      thus thesis;

    end;

    ::$Canceled

    theorem :: GRCAT_1:36



     Th35: for f,g be Morphism of ( GroupCat UN), f9,g9 be Element of ( Morphs ( GroupObjects 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 ( GroupObjects 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 = ( GroupCat UN), V = ( GroupObjects 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, Def26;

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

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

      hence

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

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



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

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

      end;

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

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

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

      hence thesis by A1, Def26;

    end;



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

    proof

      set X = ( Morphs ( GroupObjects UN));

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

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

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

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



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

      then

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



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

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

      hence thesis by A3, Th35;

    end;

    registration

      let UN;

      cluster ( GroupCat UN) -> reflexive Category-like;

      coherence

      proof

        set C = ( GroupCat UN);

        thus C is reflexive

        proof

          let a be Element of C;

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

          consider x be object such that x in UN and

           A1: GO (x,G) by Def22;

          set ii = ( ID G);

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

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

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

          reconsider ii as Morphism of C;

          reconsider ia = ii as GroupMorphismStr;



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

          .= a;

          ( cod ii) = ( cod ia) by Def26

          .= a;

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

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

        end;

        let f,g be Morphism of C;

        reconsider ff = f, gg = g as Element of ( Morphs ( GroupObjects UN));

        thus [g, f] in ( dom the Comp of C) iff ( dom g) = ( cod f) by Th35;

      end;

    end



     Lm2: for a be Element of ( GroupCat UN), aa be Element of ( GroupObjects UN) st a = aa holds for i be Morphism of a, a st i = ( ID aa) holds for b be Element of ( GroupCat 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 ( GroupCat UN), aa be Element of ( GroupObjects UN) such that a = aa;

      let i be Morphism of a, a such that

       A1: i = ( ID aa);

      let b be Element of ( GroupCat 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 ( GroupObjects UN));

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

         A3: gg is strict Morphism of G1, H1 by Def23;

        consider f be Function of G1, H1 such that

         A4: gg = GroupMorphismStr (# G1, H1, f #) by A3, Th13;



         A5: ii = GroupMorphismStr (# aa, aa, ( id aa) #) by A1;



         A6: ( cod ii) = aa by A1;



         A7: ( dom gg) = G1 by A4;



         A8: ( Hom (a,a)) <> {} ;

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

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

        then

         A9: ( dom gg) = ( cod ii) by Th35;

        then aa = ( dom gg) by A6;

        then

         A10: aa = G1 by A7;

        then

        reconsider f as Function of aa, H1;



         A11: the GroupMorphismStr of gg = GroupMorphismStr (# aa, H1, f #) by A4, A10;



         A12: [gg, ii] in ( dom ( comp ( GroupObjects UN))) by Def27, A9;

        then [g, i] in ( dom the Comp of ( GroupCat UN));



        hence (g (*) i) = (the Comp of ( GroupCat UN) . (g,i)) by CAT_1:def 1

        .= (( comp ( GroupObjects UN)) . (g,i))

        .= (gg * ii) by A12, Def27

        .= GroupMorphismStr (# aa, H1, (f * ( id aa)) #) by A5, Def14, A11, A9

        .= GroupMorphismStr (# aa, H1, f #) by FUNCT_2: 17

        .= g by A10, A4;

      end;

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

      proof

        assume

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

        let g be Morphism of b, a;

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

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

         A14: gg is strict Morphism of G1, H1 by Def23;

        consider f be Function of G1, H1 such that

         A15: gg = GroupMorphismStr (# G1, H1, f #) by A14, Th13;



         A16: ii = GroupMorphismStr (# aa, aa, ( id aa) #) by A1;



         A17: ( dom ii) = aa by A1;



         A18: ( cod gg) = H1 by A15;



         A19: ( Hom (a,a)) <> {} ;

        ( cod g) = a by A13, CAT_1: 5

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

        then

         A20: ( cod gg) = ( dom ii) by Th35;

        then aa = ( cod gg) by A17;

        then

         A21: aa = H1 by A18;

        then

        reconsider f as Function of G1, aa;



         A22: the GroupMorphismStr of gg = GroupMorphismStr (# G1, aa, f #) by A15, A21;



         A23: [ii, gg] in ( dom ( comp ( GroupObjects UN))) by Def27, A20;

        then [i, g] in ( dom the Comp of ( GroupCat UN));



        hence (i (*) g) = (the Comp of ( GroupCat UN) . (i,g)) by CAT_1:def 1

        .= (( comp ( GroupObjects UN)) . (i,g))

        .= (ii * gg) by A23, Def27

        .= GroupMorphismStr (# G1, aa, (( id aa) * f) #) by A16, Def14, A22, A20

        .= GroupMorphismStr (# G1, aa, f #) by FUNCT_2: 17

        .= g by A21, A15;

      end;

    end;

    registration

      let UN;

      cluster ( GroupCat UN) -> transitive associative with_identities;

      coherence

      proof

        set C = ( GroupCat UN);

        set X = ( Morphs ( GroupObjects UN));

        thus C is transitive

        proof

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

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

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

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



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

          then

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



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

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

          hence thesis by A3, Th35;

        end;

        thus C is associative

        proof

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

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

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



           A5: (h9 * g9) = (h (*) g) & ( dom (h (*) g)) = ( cod f) by A4, Lm1, Th35;



           A6: ( dom h9) = ( cod g9) & ( dom g9) = ( cod f9) by A4, Th35;

          then

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

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



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

          .= (hg * f9) by A6, Th22

          .= ((h (*) g) (*) f) by A5, Th35;

          hence thesis;

        end;

        thus C is with_identities

        proof

          let a be Element of C;

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

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

          reconsider ia = ii as GroupMorphismStr;



           A7: ( dom ii) = ( dom ia) by Def25

          .= a;

          ( cod ii) = ( cod ia) by Def26

          .= a;

          then

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

          take ii;

          thus thesis by Lm2;

        end;

      end;

    end

    definition

      let UN;

      :: GRCAT_1:def31

      func AbGroupObjects (UN) -> Subset of the carrier of ( GroupCat UN) equals { G where G be Element of ( GroupCat UN) : ex H be AbGroup st G = H };

      coherence

      proof

        set D2 = the carrier of ( GroupCat UN);

        now

          let x be object;

          assume x in { G where G be Element of D2 : ex H be AbGroup st G = H };

          then ex G be Element of D2 st x = G & ex H be AbGroup st G = H;

          hence x in D2;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: GRCAT_1:37



     Th36: Trivial-addLoopStr in ( AbGroupObjects UN)

    proof

       Trivial-addLoopStr in the carrier of ( GroupCat UN) by Th29;

      hence thesis;

    end;

    registration

      let UN;

      cluster ( AbGroupObjects UN) -> non empty;

      coherence by Th36;

    end

    definition

      let UN;

      :: GRCAT_1:def32

      func AbGroupCat UN -> Subcategory of ( GroupCat UN) equals ( cat ( AbGroupObjects UN));

      coherence ;

    end

    registration

      let UN;

      cluster ( AbGroupCat UN) -> strict;

      coherence ;

    end

    theorem :: GRCAT_1:38

    the carrier of ( AbGroupCat UN) = ( AbGroupObjects UN);

    definition

      let UN;

      :: GRCAT_1:def33

      func MidOpGroupObjects (UN) -> Subset of the carrier of ( AbGroupCat UN) equals { G where G be Element of ( AbGroupCat UN) : ex H be midpoint_operator AbGroup st G = H };

      coherence

      proof

        set D2 = the carrier of ( AbGroupCat UN);

        now

          let x be object;

          assume x in { G where G be Element of D2 : ex H be midpoint_operator AbGroup st G = H };

          then ex G be Element of D2 st x = G & ex H be midpoint_operator AbGroup st G = H;

          hence x in D2;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let UN;

      cluster ( MidOpGroupObjects UN) -> non empty;

      coherence

      proof

        set T = Trivial-addLoopStr ;

        set D2 = the carrier of ( AbGroupCat UN);

        set D1 = { G where G be Element of D2 : ex H be midpoint_operator AbGroup st G = H };

        T in D2 by Th36;

        then T in D1;

        then

        reconsider D1 as non empty set;

        now

          let x be set;

          assume x in D1;

          then ex G be Element of D2 st x = G & ex H be midpoint_operator AbGroup st G = H;

          hence x in D2;

        end;

        hence thesis;

      end;

    end

    definition

      let UN;

      :: GRCAT_1:def34

      func MidOpGroupCat UN -> Subcategory of ( AbGroupCat UN) equals ( cat ( MidOpGroupObjects UN));

      coherence ;

    end

    registration

      let UN;

      cluster ( MidOpGroupCat UN) -> strict;

      coherence ;

    end

    theorem :: GRCAT_1:39

    the carrier of ( MidOpGroupCat UN) = ( MidOpGroupObjects UN);

    theorem :: GRCAT_1:40

     Trivial-addLoopStr in ( MidOpGroupObjects UN)

    proof

       Trivial-addLoopStr in the carrier of ( AbGroupCat UN) by Th36;

      hence thesis;

    end;

    theorem :: GRCAT_1:41

    for S,T be non empty 1-sorted holds for f be Function of S, T st f is one-to-one onto holds (f * (f " )) = ( id T) & ((f " ) * f) = ( id S) & (f " ) is one-to-one onto

    proof

      let S,T be non empty 1-sorted;

      let f be Function of S, T;



       A1: ( [#] T) = the carrier of T;

      assume

       A2: f is one-to-one onto;

      then

       A3: ( rng f) = the carrier of T by FUNCT_2:def 3;

      then ( dom f) = the carrier of S & ( rng (f " )) = ( [#] S) by A2, A1, FUNCT_2:def 1, TOPS_2: 49;

      hence thesis by A2, A3, A1, FUNCT_2:def 3, TOPS_2: 50, TOPS_2: 52;

    end;

    theorem :: GRCAT_1:42

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

    proof

      let a be Object of ( GroupCat UN), aa be Element of ( GroupObjects UN);

      set C = ( GroupCat UN);

      assume

       A1: a = aa;

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

      reconsider ia = ii as GroupMorphismStr;



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

      .= a by A1;

      ( cod ii) = ( cod ia) by Def26

      .= 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, Lm2;

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

    end;