cat_6.miz



    begin

    definition

      struct ( 1-sorted) CategoryStr (# the carrier -> set,

the composition -> PartFunc of [: the carrier, the carrier:], the carrier #)

       attr strict strict;

    end

    reserve C for CategoryStr;

    definition

      let C;

      :: CAT_6:def1

      func Mor (C) -> set equals the carrier of C;

      correctness ;

    end

    definition

      let C;

      mode morphism of C is Element of ( Mor C);

    end

    reserve f,f1,f2,f3 for morphism of C;

    definition

      let C, f1, f2;

      :: CAT_6:def2

      pred f1,f2 are_composable means

      : Def2: [f1, f2] in ( dom the composition of C);

    end

    notation

      let C, f1, f2;

      synonym f1 |> f2 for f1,f2 are_composable ;

    end

    definition

      let C, f1, f2;

      assume

       A1: f1 |> f2;

      :: CAT_6:def3

      func f1 (*) f2 -> morphism of C equals

      : Def3: (the composition of C . (f1,f2));

      correctness

      proof

        per cases by A1;

          suppose [f1, f2] in ( dom the composition of C);

          then (the composition of C . [f1, f2]) in ( rng the composition of C) by FUNCT_1: 3;

          hence thesis by BINOP_1:def 1;

        end;

          suppose

           A2: ( Mor C) is empty;

          (the composition of C . [f1, f2]) = (the composition of C . (f1,f2)) by BINOP_1:def 1;

          hence thesis by A2, SUBSET_1:def 1;

        end;

      end;

    end

    definition

      let C, f;

      :: CAT_6:def4

      attr f is left_identity means

      : Def4: for f1 be morphism of C st f |> f1 holds (f (*) f1) = f1;

      :: CAT_6:def5

      attr f is right_identity means

      : Def5: for f1 be morphism of C st f1 |> f holds (f1 (*) f) = f1;

    end

    definition

      let C;

      :: CAT_6:def6

      attr C is with_left_identities means

      : Def6: for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f |> f1 & f is left_identity;

      :: CAT_6:def7

      attr C is with_right_identities means

      : Def7: for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f1 |> f & f is right_identity;

      :: CAT_6:def8

      attr C is left_composable means for f,f1,f2 be morphism of C st f1 |> f2 holds (f1 (*) f2) |> f iff f2 |> f;

      :: CAT_6:def9

      attr C is right_composable means

      : Def9: for f,f1,f2 be morphism of C st f1 |> f2 holds f |> (f1 (*) f2) iff f |> f1;

      :: CAT_6:def10

      attr C is associative means

      : Def10: for f1,f2,f3 be morphism of C st f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) holds (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3);

    end

    definition

      let C;

      :: CAT_6:def11

      attr C is composable means

      : Def11: C is left_composable right_composable;

      :: CAT_6:def12

      attr C is with_identities means

      : Def12: C is with_left_identities with_right_identities;

    end

    definition

      let C;

      :: CAT_6:def13

      func C opp -> strict CategoryStr equals CategoryStr (# the carrier of C, ( ~ the composition of C) #);

      coherence ;

    end

    theorem :: CAT_6:1

    C is empty implies not f1 |> f2;

    reserve g1,g2 for morphism of (C opp );

    theorem :: CAT_6:2

    f1 = g1 & f2 = g2 implies (f1 |> f2 iff g2 |> g1) by FUNCT_4: 42;

    theorem :: CAT_6:3

    

     Th3: f1 = g1 & f2 = g2 & f1 |> f2 implies (f1 (*) f2) = (g2 (*) g1)

    proof

      assume

       A1: f1 = g1 & f2 = g2;

      assume

       A2: f1 |> f2;

      

       A3: g2 |> g1 by A1, A2, FUNCT_4: 42;

      

      thus (f1 (*) f2) = (the composition of C . (f1,f2)) by A2, Def3

      .= (( ~ the composition of C) . (f2,f1)) by A2, FUNCT_4:def 2

      .= (g2 (*) g1) by A1, A3, Def3;

    end;

    theorem :: CAT_6:4

    

     Th4: C is left_composable iff (C opp ) is right_composable

    proof

      hereby

        assume

         A1: C is left_composable;

        for g,g1,g2 be morphism of (C opp ) st g1 |> g2 holds (g |> (g1 (*) g2) iff g |> g1)

        proof

          let g,g1,g2 be morphism of (C opp );

          reconsider f = g, f2 = g1, f1 = g2 as morphism of C;

          assume g1 |> g2;

          then

           A2: f1 |> f2 by FUNCT_4: 42;

          then

           A3: (f1 (*) f2) = (g1 (*) g2) by Th3;

          hereby

            assume g |> (g1 (*) g2);

            then (f1 (*) f2) |> f by A3, FUNCT_4: 42;

            then f2 |> f by A1, A2;

            hence g |> g1 by FUNCT_4: 42;

          end;

          assume g |> g1;

          then f2 |> f by FUNCT_4: 42;

          then (f1 (*) f2) |> f by A1, A2;

          hence g |> (g1 (*) g2) by A3, FUNCT_4: 42;

        end;

        hence (C opp ) is right_composable;

      end;

      assume

       A4: (C opp ) is right_composable;

      for f,f1,f2 be morphism of C st f1 |> f2 holds ((f1 (*) f2) |> f iff f2 |> f)

      proof

        let f,f1,f2 be morphism of C;

        reconsider g = f, g2 = f1, g1 = f2 as morphism of (C opp );

        assume

         A5: f1 |> f2;

        then

         A6: g1 |> g2 by FUNCT_4: 42;

        

         A7: (f1 (*) f2) = (g1 (*) g2) by A5, Th3;

        hereby

          assume (f1 (*) f2) |> f;

          then g |> (g1 (*) g2) by A7, FUNCT_4: 42;

          then g |> g1 by A4, A6;

          hence f2 |> f by FUNCT_4: 42;

        end;

        assume f2 |> f;

        then g |> g1 by FUNCT_4: 42;

        then g |> (g1 (*) g2) by A4, A6;

        hence (f1 (*) f2) |> f by A7, FUNCT_4: 42;

      end;

      hence C is left_composable;

    end;

    theorem :: CAT_6:5

    

     Th5: C is right_composable iff (C opp ) is left_composable

    proof

      hereby

        assume

         A1: C is right_composable;

        for g,g1,g2 be morphism of (C opp ) st g1 |> g2 holds ((g1 (*) g2) |> g iff g2 |> g)

        proof

          let g,g1,g2 be morphism of (C opp );

          reconsider f = g, f2 = g1, f1 = g2 as morphism of C;

          assume g1 |> g2;

          then

           A2: f1 |> f2 by FUNCT_4: 42;

          then

           A3: (f1 (*) f2) = (g1 (*) g2) by Th3;

          hereby

            assume (g1 (*) g2) |> g;

            then f |> (f1 (*) f2) by A3, FUNCT_4: 42;

            then f |> f1 by A1, A2;

            hence g2 |> g by FUNCT_4: 42;

          end;

          assume g2 |> g;

          then f |> f1 by FUNCT_4: 42;

          then f |> (f1 (*) f2) by A1, A2;

          hence (g1 (*) g2) |> g by A3, FUNCT_4: 42;

        end;

        hence (C opp ) is left_composable;

      end;

      assume

       A4: (C opp ) is left_composable;

      for f,f1,f2 be morphism of C st f1 |> f2 holds (f |> (f1 (*) f2) iff f |> f1)

      proof

        let f,f1,f2 be morphism of C;

        reconsider g = f, g2 = f1, g1 = f2 as morphism of (C opp );

        assume

         A5: f1 |> f2;

        then

         A6: g1 |> g2 by FUNCT_4: 42;

        

         A7: (f1 (*) f2) = (g1 (*) g2) by A5, Th3;

        hereby

          assume f |> (f1 (*) f2);

          then (g1 (*) g2) |> g by A7, FUNCT_4: 42;

          then g2 |> g by A4, A6;

          hence f |> f1 by FUNCT_4: 42;

        end;

        assume f |> f1;

        then g2 |> g by FUNCT_4: 42;

        then (g1 (*) g2) |> g by A4, A6;

        hence f |> (f1 (*) f2) by A7, FUNCT_4: 42;

      end;

      hence C is right_composable;

    end;

    theorem :: CAT_6:6

    

     Th6: C is with_left_identities iff (C opp ) is with_right_identities

    proof

      hereby

        assume

         A1: C is with_left_identities;

        for g1 be morphism of (C opp ) st g1 in the carrier of (C opp ) holds ex g be morphism of (C opp ) st g1 |> g & g is right_identity

        proof

          let g1 be morphism of (C opp );

          assume

           A2: g1 in the carrier of (C opp );

          reconsider f1 = g1 as morphism of C;

          consider f be morphism of C such that

           A3: f |> f1 & f is left_identity by A1, A2;

          reconsider g = f as morphism of (C opp );

          take g;

          thus g1 |> g by A3, FUNCT_4: 42;

          for g2 be morphism of (C opp ) st g2 |> g holds (g2 (*) g) = g2

          proof

            let g2 be morphism of (C opp );

            reconsider f2 = g2 as morphism of C;

            assume g2 |> g;

            then

             A4: f |> f2 by FUNCT_4: 42;

            then (f (*) f2) = f2 by A3;

            hence (g2 (*) g) = g2 by A4, Th3;

          end;

          hence g is right_identity;

        end;

        hence (C opp ) is with_right_identities;

      end;

      assume

       A5: (C opp ) is with_right_identities;

      for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f |> f1 & f is left_identity

      proof

        let f1 be morphism of C;

        assume

         A6: f1 in the carrier of C;

        reconsider g1 = f1 as morphism of (C opp );

        consider g be morphism of (C opp ) such that

         A7: g1 |> g & g is right_identity by A5, A6;

        reconsider f = g as morphism of C;

        take f;

        thus f |> f1 by A7, FUNCT_4: 42;

        for f2 be morphism of C st f |> f2 holds (f (*) f2) = f2

        proof

          let f2 be morphism of C;

          reconsider g2 = f2 as morphism of (C opp );

          assume

           A8: f |> f2;

          then g2 |> g by FUNCT_4: 42;

          then (g2 (*) g) = g2 by A7;

          hence (f (*) f2) = f2 by A8, Th3;

        end;

        hence f is left_identity;

      end;

      hence C is with_left_identities;

    end;

    theorem :: CAT_6:7

    

     Th7: C is with_right_identities iff (C opp ) is with_left_identities

    proof

      hereby

        assume

         A1: C is with_right_identities;

        for g1 be morphism of (C opp ) st g1 in the carrier of (C opp ) holds ex g be morphism of (C opp ) st g |> g1 & g is left_identity

        proof

          let g1 be morphism of (C opp );

          assume

           A2: g1 in the carrier of (C opp );

          reconsider f1 = g1 as morphism of C;

          consider f be morphism of C such that

           A3: f1 |> f & f is right_identity by A1, A2;

          reconsider g = f as morphism of (C opp );

          take g;

          thus g |> g1 by A3, FUNCT_4: 42;

          for g2 be morphism of (C opp ) st g |> g2 holds (g (*) g2) = g2

          proof

            let g2 be morphism of (C opp );

            reconsider f2 = g2 as morphism of C;

            assume g |> g2;

            then

             A4: f2 |> f by FUNCT_4: 42;

            then (f2 (*) f) = f2 by A3;

            hence (g (*) g2) = g2 by A4, Th3;

          end;

          hence g is left_identity;

        end;

        hence (C opp ) is with_left_identities;

      end;

      assume

       A5: (C opp ) is with_left_identities;

      for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f1 |> f & f is right_identity

      proof

        let f1 be morphism of C;

        assume

         A6: f1 in the carrier of C;

        reconsider g1 = f1 as morphism of (C opp );

        consider g be morphism of (C opp ) such that

         A7: g |> g1 & g is left_identity by A5, A6;

        reconsider f = g as morphism of C;

        take f;

        thus f1 |> f by A7, FUNCT_4: 42;

        for f2 be morphism of C st f2 |> f holds (f2 (*) f) = f2

        proof

          let f2 be morphism of C;

          reconsider g2 = f2 as morphism of (C opp );

          assume

           A8: f2 |> f;

          then g |> g2 by FUNCT_4: 42;

          then (g (*) g2) = g2 by A7;

          hence (f2 (*) f) = f2 by A8, Th3;

        end;

        hence f is right_identity;

      end;

      hence C is with_right_identities;

    end;

    theorem :: CAT_6:8

    

     Th8: C is associative iff (C opp ) is associative

    proof

      hereby

        assume

         A1: C is associative;

        for g1,g2,g3 be morphism of (C opp ) st g1 |> g2 & g2 |> g3 & (g1 (*) g2) |> g3 & g1 |> (g2 (*) g3) holds (g1 (*) (g2 (*) g3)) = ((g1 (*) g2) (*) g3)

        proof

          let g1,g2,g3 be morphism of (C opp );

          reconsider f3 = g1, f2 = g2, f1 = g3 as morphism of C;

          assume g1 |> g2;

          then

           A2: f2 |> f3 by FUNCT_4: 42;

          assume g2 |> g3;

          then

           A3: f1 |> f2 by FUNCT_4: 42;

          assume

           A4: (g1 (*) g2) |> g3;

          assume

           A5: g1 |> (g2 (*) g3);

          

           A6: (g1 (*) g2) = (f2 (*) f3) by A2, Th3;

          then

           A7: f1 |> (f2 (*) f3) by A4, FUNCT_4: 42;

          

           A8: (f1 (*) f2) = (g2 (*) g3) by A3, Th3;

          then

           A9: (f1 (*) f2) |> f3 by A5, FUNCT_4: 42;

          

          thus (g1 (*) (g2 (*) g3)) = ((f1 (*) f2) (*) f3) by A8, A9, Th3

          .= (f1 (*) (f2 (*) f3)) by A1, A2, A3, A7, A9

          .= ((g1 (*) g2) (*) g3) by A6, A7, Th3;

        end;

        hence (C opp ) is associative;

      end;

      assume

       A10: (C opp ) is associative;

      for f1,f2,f3 be morphism of C st f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) holds (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3)

      proof

        let f1,f2,f3 be morphism of C;

        reconsider g3 = f1, g2 = f2, g1 = f3 as morphism of (C opp );

        assume

         A11: f1 |> f2;

        then

         A12: g2 |> g3 by FUNCT_4: 42;

        assume

         A13: f2 |> f3;

        then

         A14: g1 |> g2 by FUNCT_4: 42;

        assume

         A15: (f1 (*) f2) |> f3;

        assume

         A16: f1 |> (f2 (*) f3);

        

         A17: (f1 (*) f2) = (g2 (*) g3) by A11, Th3;

        then

         A18: g1 |> (g2 (*) g3) by A15, FUNCT_4: 42;

        

         A19: (g1 (*) g2) = (f2 (*) f3) by A13, Th3;

        then

         A20: (g1 (*) g2) |> g3 by A16, FUNCT_4: 42;

        

        thus (f1 (*) (f2 (*) f3)) = ((g1 (*) g2) (*) g3) by A19, A16, Th3

        .= (g1 (*) (g2 (*) g3)) by A10, A12, A14, A18, A20

        .= ((f1 (*) f2) (*) f3) by A17, A15, Th3;

      end;

      hence C is associative;

    end;

    registration

      cluster with_left_identities non with_right_identities composable associative for CategoryStr;

      correctness

      proof

        reconsider X = { 0 , 1} as set;

        set comp = { [ [ 0 , 0 ], 0 ], [ [ 0 , 1], 1]};

        

         A1: for x,y1,y2 be object st [x, y1] in comp & [x, y2] in comp holds y1 = y2

        proof

          let x,y1,y2 be object;

          assume

           A2: [x, y1] in comp;

          assume

           A3: [x, y2] in comp;

          per cases by A2, TARSKI:def 2;

            suppose

             A4: [x, y1] = [ [ 0 , 0 ], 0 ];

            then

             A5: x = [ 0 , 0 ] & y1 = 0 by XTUPLE_0: 1;

            per cases by A3, TARSKI:def 2;

              suppose [x, y2] = [ [ 0 , 0 ], 0 ];

              hence thesis by A4, XTUPLE_0: 1;

            end;

              suppose [x, y2] = [ [ 0 , 1], 1];

              then x = [ 0 , 1] & y2 = 1 by XTUPLE_0: 1;

              hence thesis by A5, XTUPLE_0: 1;

            end;

          end;

            suppose

             A6: [x, y1] = [ [ 0 , 1], 1];

            then

             A7: x = [ 0 , 1] & y1 = 1 by XTUPLE_0: 1;

            per cases by A3, TARSKI:def 2;

              suppose [x, y2] = [ [ 0 , 0 ], 0 ];

              then x = [ 0 , 0 ] & y2 = 0 by XTUPLE_0: 1;

              hence thesis by A7, XTUPLE_0: 1;

            end;

              suppose [x, y2] = [ [ 0 , 1], 1];

              hence thesis by A6, XTUPLE_0: 1;

            end;

          end;

        end;

        for x be object st x in comp holds x in [: [:X, X:], X:]

        proof

          let x be object;

          assume

           A8: x in comp;

          per cases by A8, TARSKI:def 2;

            suppose

             A9: x = [ [ 0 , 0 ], 0 ];

            

             A10: 0 in X by TARSKI:def 2;

            then [ 0 , 0 ] in [:X, X:] by ZFMISC_1:def 2;

            hence x in [: [:X, X:], X:] by A9, A10, ZFMISC_1:def 2;

          end;

            suppose

             A11: x = [ [ 0 , 1], 1];

            

             A12: 0 in X & 1 in X by TARSKI:def 2;

            then [ 0 , 1] in [:X, X:] by ZFMISC_1:def 2;

            hence x in [: [:X, X:], X:] by A11, A12, ZFMISC_1:def 2;

          end;

        end;

        then

        reconsider comp as PartFunc of [:X, X:], X by A1, TARSKI:def 3, FUNCT_1:def 1;

        set C = CategoryStr (# X, comp #);

        

         A13: for f1,f2 be morphism of C st f1 |> f2 holds (f1 = 0 & f2 = 0 & (f1 (*) f2) = 0 ) or (f1 = 0 & f2 = 1 & (f1 (*) f2) = 1)

        proof

          let f1,f2 be morphism of C;

          assume

           A14: f1 |> f2;

          assume

           A15: not (f1 = 0 & f2 = 0 & (f1 (*) f2) = 0 );

          consider y be object such that

           A16: [ [f1, f2], y] in the composition of C by A14, XTUPLE_0:def 12;

          

           A17: (f1 (*) f2) = (the composition of C . (f1,f2)) by Def3, A14

          .= (the composition of C . [f1, f2]) by BINOP_1:def 1

          .= y by A16, FUNCT_1: 1;

          per cases by A16, TARSKI:def 2;

            suppose [ [f1, f2], y] = [ [ 0 , 0 ], 0 ];

            then [f1, f2] = [ 0 , 0 ] & y = 0 by XTUPLE_0: 1;

            hence thesis by A17, A15, XTUPLE_0: 1;

          end;

            suppose [ [f1, f2], y] = [ [ 0 , 1], 1];

            then [f1, f2] = [ 0 , 1] & y = 1 by XTUPLE_0: 1;

            hence thesis by A17, XTUPLE_0: 1;

          end;

        end;

        

         A18: for f1,f2 be morphism of C st f1 |> f2 holds f1 = 0 & (f2 = 0 or f2 = 1)

        proof

          let f1,f2 be morphism of C;

          assume f1 |> f2;

          then

          consider y be object such that

           A19: [ [f1, f2], y] in the composition of C by XTUPLE_0:def 12;

          per cases by A19, TARSKI:def 2;

            suppose [ [f1, f2], y] = [ [ 0 , 0 ], 0 ];

            then [f1, f2] = [ 0 , 0 ] & y = 0 by XTUPLE_0: 1;

            hence thesis by XTUPLE_0: 1;

          end;

            suppose [ [f1, f2], y] = [ [ 0 , 1], 1];

            then [f1, f2] = [ 0 , 1] & y = 1 by XTUPLE_0: 1;

            hence thesis by XTUPLE_0: 1;

          end;

        end;

        

         A20: for f1,f2 be morphism of C st f1 = 0 holds f1 |> f2

        proof

          let f1,f2 be morphism of C;

          assume

           A21: f1 = 0 ;

          f2 = 0 or f2 = 1 by TARSKI:def 2;

          then [ [f1, f2], f2] in the composition of C by A21, TARSKI:def 2;

          hence thesis by FUNCT_1: 1;

        end;

        for f,f1,f2 be morphism of C st f1 |> f2 holds (f1 (*) f2) |> f iff f2 |> f

        proof

          let f,f1,f2 be morphism of C;

          assume

           A22: f1 |> f2;

          per cases by A22, A13;

            suppose f1 = 0 & f2 = 0 & (f1 (*) f2) = 0 ;

            hence thesis;

          end;

            suppose f1 = 0 & f2 = 1 & (f1 (*) f2) = 1;

            hence thesis;

          end;

        end;

        then

         A23: C is left_composable;

        for f,f1,f2 be morphism of C st f1 |> f2 holds f |> (f1 (*) f2) iff f |> f1

        proof

          let f,f1,f2 be morphism of C;

          assume

           A24: f1 |> f2;

          per cases by A24, A13;

            suppose f1 = 0 & f2 = 0 & (f1 (*) f2) = 0 ;

            hence thesis;

          end;

            suppose f1 = 0 & f2 = 1 & (f1 (*) f2) = 1;

            hereby

              assume f |> (f1 (*) f2);

              then f = 0 by A18;

              hence f |> f1 by A20;

            end;

            assume f |> f1;

            then f = 0 by A18;

            hence f |> (f1 (*) f2) by A20;

          end;

        end;

        then

         A25: C is composable by A23, Def9;

        for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f |> f1 & f is left_identity

        proof

          let f1 be morphism of C;

          assume f1 in the carrier of C;

          reconsider f = 0 as morphism of C by TARSKI:def 2;

          take f;

          thus f |> f1 by A20;

          for f2 be morphism of C st f |> f2 holds (f (*) f2) = f2

          proof

            let f2 be morphism of C;

            assume

             A26: f |> f2;

            f2 = 0 or f2 = 1 by TARSKI:def 2;

            hence (f (*) f2) = f2 by A26, A13;

          end;

          hence f is left_identity;

        end;

        then

         A27: C is with_left_identities;

        ex f1 be morphism of C st f1 in the carrier of C & for f be morphism of C st f1 |> f holds not f is right_identity

        proof

          reconsider f1 = 1 as morphism of C by TARSKI:def 2;

          take f1;

          thus f1 in the carrier of C;

          let f be morphism of C;

          assume f1 |> f;

          hence thesis by A18;

        end;

        then

         A28: C is non with_right_identities;

        for f1,f2,f3 be morphism of C st f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) holds (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3)

        proof

          let f1,f2,f3 be morphism of C;

          assume

           A29: f1 |> f2 & f2 |> f3;

          assume

           A30: (f1 (*) f2) |> f3;

          assume

           A31: f1 |> (f2 (*) f3);

          per cases by TARSKI:def 2;

            suppose

             A32: f3 = 0 ;

            then (f2 (*) f3) = 0 by A29, A13;

            

            hence (f1 (*) (f2 (*) f3)) = 0 by A31, A13

            .= ((f1 (*) f2) (*) f3) by A30, A32, A13;

          end;

            suppose

             A33: f3 = 1;

            then (f2 (*) f3) = 1 by A29, A13;

            

            hence (f1 (*) (f2 (*) f3)) = 1 by A31, A13

            .= ((f1 (*) f2) (*) f3) by A30, A33, A13;

          end;

        end;

        hence thesis by A25, A27, A28, Def10;

      end;

    end

    registration

      cluster non with_left_identities with_right_identities composable associative for CategoryStr;

      correctness

      proof

        set C1 = the with_left_identities non with_right_identities composable associative CategoryStr;

        set C = (C1 opp );

        take C;

        thus C is non with_left_identities by Th7;

        thus C is with_right_identities by Th6;

        thus C is composable by Th4, Th5, Def11;

        thus thesis by Th8;

      end;

    end

    registration

      cluster non left_composable right_composable with_identities associative for CategoryStr;

      correctness

      proof

        set X1 = ( NAT \ { 0 });

        set X2 = { [n1, n2] where n1,n2 be Element of NAT : n2 = (n1 + 1) };

        reconsider X = (X1 \/ X2) as set;

        set c0 = { [ [ [n1, n2], [n1, n2]], [n1, n2]] where n1,n2 be Element of NAT : n2 = (n1 + 1) };

        set c1 = { [ [ [n1, n2], n2], n2] where n1,n2 be Element of NAT : n2 = (n1 + 1) };

        set c2 = { [ [n1, [n1, n2]], n1] where n1,n2 be Element of NAT : n2 = (n1 + 1) & n1 <> 0 };

        set c3 = { [ [n1, n2], n1] where n1,n2 be Element of NAT : n2 = (n1 + 1) & n1 <> 0 };

        set comp = (((c0 \/ c1) \/ c2) \/ c3);

        1 in NAT & not 1 in { 0 } by TARSKI:def 1;

        then

         A1: 1 in X1 by XBOOLE_0:def 5;

        

         A2: for x,y1,y2 be object st [x, y1] in comp & [x, y2] in comp holds y1 = y2

        proof

          let x,y1,y2 be object;

          assume [x, y1] in comp;

          then [x, y1] in ((c0 \/ c1) \/ c2) or [x, y1] in c3 by XBOOLE_0:def 3;

          then

           A3: [x, y1] in (c0 \/ c1) or [x, y1] in c2 or [x, y1] in c3 by XBOOLE_0:def 3;

          assume [x, y2] in comp;

          then [x, y2] in ((c0 \/ c1) \/ c2) or [x, y2] in c3 by XBOOLE_0:def 3;

          then

           A4: [x, y2] in (c0 \/ c1) or [x, y2] in c2 or [x, y2] in c3 by XBOOLE_0:def 3;

          per cases by A3, XBOOLE_0:def 3;

            suppose [x, y1] in c0;

            then

            consider n11,n12 be Element of NAT such that

             A5: [x, y1] = [ [ [n11, n12], [n11, n12]], [n11, n12]] & n12 = (n11 + 1);

            

             A6: x = [ [n11, n12], [n11, n12]] & y1 = [n11, n12] by A5, XTUPLE_0: 1;

            per cases by A4, XBOOLE_0:def 3;

              suppose [x, y2] in c0;

              then

              consider n21,n22 be Element of NAT such that

               A7: [x, y2] = [ [ [n21, n22], [n21, n22]], [n21, n22]] & n22 = (n21 + 1);

              x = [ [n21, n22], [n21, n22]] & y2 = [n21, n22] by A7, XTUPLE_0: 1;

              hence thesis by A6, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c1;

              then

              consider n21,n22 be Element of NAT such that

               A8: [x, y2] = [ [ [n21, n22], n22], n22] & n22 = (n21 + 1);

              x = [ [n21, n22], n22] & y2 = n22 by A8, XTUPLE_0: 1;

              hence thesis by A6, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c2;

              then

              consider n21,n22 be Element of NAT such that

               A9: [x, y2] = [ [n21, [n21, n22]], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, [n21, n22]] & y2 = n21 by A9, XTUPLE_0: 1;

              hence thesis by A6, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c3;

              then

              consider n21,n22 be Element of NAT such that

               A10: [x, y2] = [ [n21, n22], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, n22] & y2 = n21 by A10, XTUPLE_0: 1;

              hence thesis by A6, XTUPLE_0: 1;

            end;

          end;

            suppose [x, y1] in c1;

            then

            consider n11,n12 be Element of NAT such that

             A11: [x, y1] = [ [ [n11, n12], n12], n12] & n12 = (n11 + 1);

            

             A12: x = [ [n11, n12], n12] & y1 = n12 by A11, XTUPLE_0: 1;

            per cases by A4, XBOOLE_0:def 3;

              suppose [x, y2] in c0;

              then

              consider n21,n22 be Element of NAT such that

               A13: [x, y2] = [ [ [n21, n22], [n21, n22]], [n21, n22]] & n22 = (n21 + 1);

              x = [ [n21, n22], [n21, n22]] & y2 = [n21, n22] by A13, XTUPLE_0: 1;

              hence thesis by A12, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c1;

              then

              consider n21,n22 be Element of NAT such that

               A14: [x, y2] = [ [ [n21, n22], n22], n22] & n22 = (n21 + 1);

              x = [ [n21, n22], n22] & y2 = n22 by A14, XTUPLE_0: 1;

              hence thesis by A12, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c2;

              then

              consider n21,n22 be Element of NAT such that

               A15: [x, y2] = [ [n21, [n21, n22]], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, [n21, n22]] & y2 = n21 by A15, XTUPLE_0: 1;

              hence thesis by A12, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c3;

              then

              consider n21,n22 be Element of NAT such that

               A16: [x, y2] = [ [n21, n22], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, n22] & y2 = n21 by A16, XTUPLE_0: 1;

              hence thesis by A12, XTUPLE_0: 1;

            end;

          end;

            suppose [x, y1] in c2;

            then

            consider n11,n12 be Element of NAT such that

             A17: [x, y1] = [ [n11, [n11, n12]], n11] & n12 = (n11 + 1) & n11 <> 0 ;

            

             A18: x = [n11, [n11, n12]] & y1 = n11 by A17, XTUPLE_0: 1;

            per cases by A4, XBOOLE_0:def 3;

              suppose [x, y2] in c0;

              then

              consider n21,n22 be Element of NAT such that

               A19: [x, y2] = [ [ [n21, n22], [n21, n22]], [n21, n22]] & n22 = (n21 + 1);

              x = [ [n21, n22], [n21, n22]] & y2 = [n21, n22] by A19, XTUPLE_0: 1;

              hence thesis by A18, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c1;

              then

              consider n21,n22 be Element of NAT such that

               A20: [x, y2] = [ [ [n21, n22], n22], n22] & n22 = (n21 + 1);

              x = [ [n21, n22], n22] & y2 = n22 by A20, XTUPLE_0: 1;

              hence thesis by A18, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c2;

              then

              consider n21,n22 be Element of NAT such that

               A21: [x, y2] = [ [n21, [n21, n22]], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, [n21, n22]] & y2 = n21 by A21, XTUPLE_0: 1;

              hence thesis by A18, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c3;

              then

              consider n21,n22 be Element of NAT such that

               A22: [x, y2] = [ [n21, n22], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, n22] & y2 = n21 by A22, XTUPLE_0: 1;

              hence thesis by A18, XTUPLE_0: 1;

            end;

          end;

            suppose [x, y1] in c3;

            then

            consider n11,n12 be Element of NAT such that

             A23: [x, y1] = [ [n11, n12], n11] & n12 = (n11 + 1) & n11 <> 0 ;

            

             A24: x = [n11, n12] & y1 = n11 by A23, XTUPLE_0: 1;

            per cases by A4, XBOOLE_0:def 3;

              suppose [x, y2] in c0;

              then

              consider n21,n22 be Element of NAT such that

               A25: [x, y2] = [ [ [n21, n22], [n21, n22]], [n21, n22]] & n22 = (n21 + 1);

              x = [ [n21, n22], [n21, n22]] & y2 = [n21, n22] by A25, XTUPLE_0: 1;

              hence thesis by A24, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c1;

              then

              consider n21,n22 be Element of NAT such that

               A26: [x, y2] = [ [ [n21, n22], n22], n22] & n22 = (n21 + 1);

              x = [ [n21, n22], n22] & y2 = n22 by A26, XTUPLE_0: 1;

              hence thesis by A24, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c2;

              then

              consider n21,n22 be Element of NAT such that

               A27: [x, y2] = [ [n21, [n21, n22]], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, [n21, n22]] & y2 = n21 by A27, XTUPLE_0: 1;

              hence thesis by A24, XTUPLE_0: 1;

            end;

              suppose [x, y2] in c3;

              then

              consider n21,n22 be Element of NAT such that

               A28: [x, y2] = [ [n21, n22], n21] & n22 = (n21 + 1) & n21 <> 0 ;

              x = [n21, n22] & y2 = n21 by A28, XTUPLE_0: 1;

              hence thesis by A24, XTUPLE_0: 1;

            end;

          end;

        end;

        for x be object st x in comp holds x in [: [:X, X:], X:]

        proof

          let x be object;

          assume x in comp;

          then x in ((c0 \/ c1) \/ c2) or x in c3 by XBOOLE_0:def 3;

          then

           A29: x in (c0 \/ c1) or x in c2 or x in c3 by XBOOLE_0:def 3;

          per cases by A29, XBOOLE_0:def 3;

            suppose x in c0;

            then

            consider n1,n2 be Element of NAT such that

             A30: x = [ [ [n1, n2], [n1, n2]], [n1, n2]] & n2 = (n1 + 1);

             [n1, n2] in X2 by A30;

            then

             A31: [n1, n2] in X by XBOOLE_0:def 3;

            then [ [n1, n2], [n1, n2]] in [:X, X:] by ZFMISC_1:def 2;

            hence x in [: [:X, X:], X:] by A30, A31, ZFMISC_1:def 2;

          end;

            suppose x in c1;

            then

            consider n1,n2 be Element of NAT such that

             A32: x = [ [ [n1, n2], n2], n2] & n2 = (n1 + 1);

             [n1, n2] in X2 by A32;

            then

             A33: [n1, n2] in X by XBOOLE_0:def 3;

             not n2 in { 0 } by A32, TARSKI:def 1;

            then n2 in X1 by XBOOLE_0:def 5;

            then

             A34: n2 in X by XBOOLE_0:def 3;

             [ [n1, n2], n2] in [:X, X:] by A33, A34, ZFMISC_1:def 2;

            hence x in [: [:X, X:], X:] by A32, A34, ZFMISC_1:def 2;

          end;

            suppose x in c2;

            then

            consider n1,n2 be Element of NAT such that

             A35: x = [ [n1, [n1, n2]], n1] & n2 = (n1 + 1) & n1 <> 0 ;

             [n1, n2] in X2 by A35;

            then

             A36: [n1, n2] in X by XBOOLE_0:def 3;

             not n1 in { 0 } by A35, TARSKI:def 1;

            then n1 in X1 by XBOOLE_0:def 5;

            then

             A37: n1 in X by XBOOLE_0:def 3;

             [n1, [n1, n2]] in [:X, X:] by A36, A37, ZFMISC_1:def 2;

            hence x in [: [:X, X:], X:] by A35, A37, ZFMISC_1:def 2;

          end;

            suppose x in c3;

            then

            consider n1,n2 be Element of NAT such that

             A38: x = [ [n1, n2], n1] & n2 = (n1 + 1) & n1 <> 0 ;

             not n1 in { 0 } by A38, TARSKI:def 1;

            then n1 in X1 by XBOOLE_0:def 5;

            then

             A39: n1 in X by XBOOLE_0:def 3;

             not n2 in { 0 } by A38, TARSKI:def 1;

            then n2 in X1 by XBOOLE_0:def 5;

            then

             A40: n2 in X by XBOOLE_0:def 3;

             [n1, n2] in [:X, X:] by A39, A40, ZFMISC_1:def 2;

            hence x in [: [:X, X:], X:] by A38, A39, ZFMISC_1:def 2;

          end;

        end;

        then

        reconsider comp as PartFunc of [:X, X:], X by A2, TARSKI:def 3, FUNCT_1:def 1;

        set C = CategoryStr (# X, comp #);

        

         A41: for n1 be Element of NAT st n1 <> 0 holds n1 is morphism of C

        proof

          let n1 be Element of NAT ;

          assume n1 <> 0 ;

          then not n1 in { 0 } by TARSKI:def 1;

          then n1 in X1 by XBOOLE_0:def 5;

          hence n1 is morphism of C by XBOOLE_0:def 3;

        end;

        

         A42: for f1,f2 be morphism of C, n1,n2 be Element of NAT st f1 = n1 & f2 = n2 & n2 = (n1 + 1) & n1 <> 0 holds f1 |> f2 & (f1 (*) f2) = f1

        proof

          let f1,f2 be morphism of C;

          let n1,n2 be Element of NAT ;

          assume

           A43: f1 = n1 & f2 = n2;

          assume n2 = (n1 + 1) & n1 <> 0 ;

          then

           A44: [ [n1, n2], n1] in c3;

          then

           A45: [ [n1, n2], n1] in (((c0 \/ c1) \/ c2) \/ c3) by XBOOLE_0:def 3;

          

           A46: [ [n1, n2], n1] in the composition of C by A44, XBOOLE_0:def 3;

          

           A47: [f1, f2] in ( dom the composition of C) by A43, A45, XTUPLE_0:def 12;

          thus f1 |> f2 by A43, A45, XTUPLE_0:def 12;

          

          thus (f1 (*) f2) = (the composition of C . (f1,f2)) by A47, Def2, Def3

          .= (the composition of C . [n1, n2]) by A43, BINOP_1:def 1

          .= f1 by A46, A43, FUNCT_1: 1;

        end;

        

         A48: for f be morphism of C st f in X2 holds f is left_identity & f is right_identity & f |> f

        proof

          let f be morphism of C;

          assume f in X2;

          then

          consider nf1,nf2 be Element of NAT such that

           A49: f = [nf1, nf2] & nf2 = (nf1 + 1);

          for f1 be morphism of C st f |> f1 holds (f (*) f1) = f1

          proof

            let f1 be morphism of C;

            assume

             A50: f |> f1;

            then

            consider y be object such that

             A51: [ [f, f1], y] in the composition of C by XTUPLE_0:def 12;

             [ [f, f1], y] in ((c0 \/ c1) \/ c2) or [ [f, f1], y] in c3 by A51, XBOOLE_0:def 3;

            then

             A52: [ [f, f1], y] in (c0 \/ c1) or [ [f, f1], y] in c2 or [ [f, f1], y] in c3 by XBOOLE_0:def 3;

            per cases by A52, XBOOLE_0:def 3;

              suppose [ [f, f1], y] in c0;

              then

              consider n1,n2 be Element of NAT such that

               A53: [ [f, f1], y] = [ [ [n1, n2], [n1, n2]], [n1, n2]] & n2 = (n1 + 1);

               [f, f1] = [ [n1, n2], [n1, n2]] & y = [n1, n2] by A53, XTUPLE_0: 1;

              then

               A54: f = [n1, n2] & f1 = [n1, n2] by XTUPLE_0: 1;

              

              thus (f (*) f1) = (the composition of C . (f,f1)) by A50, Def3

              .= (the composition of C . [f, f1]) by BINOP_1:def 1

              .= f1 by A54, A51, FUNCT_1: 1, A53;

            end;

              suppose [ [f, f1], y] in c1;

              then

              consider n1,n2 be Element of NAT such that

               A55: [ [f, f1], y] = [ [ [n1, n2], n2], n2] & n2 = (n1 + 1);

               [f, f1] = [ [n1, n2], n2] & y = n2 by A55, XTUPLE_0: 1;

              then

               A56: f = [n1, n2] & f1 = n2 by XTUPLE_0: 1;

              

              thus (f (*) f1) = (the composition of C . (f,f1)) by A50, Def3

              .= (the composition of C . [f, f1]) by BINOP_1:def 1

              .= f1 by A56, A51, FUNCT_1: 1, A55;

            end;

              suppose [ [f, f1], y] in c2;

              then

              consider n1,n2 be Element of NAT such that

               A57: [ [f, f1], y] = [ [n1, [n1, n2]], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f, f1] = [n1, [n1, n2]] by A57, XTUPLE_0: 1;

              hence thesis by A49, XTUPLE_0: 1;

            end;

              suppose [ [f, f1], y] in c3;

              then

              consider n1,n2 be Element of NAT such that

               A58: [ [f, f1], y] = [ [n1, n2], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f, f1] = [n1, n2] by A58, XTUPLE_0: 1;

              hence thesis by A49, XTUPLE_0: 1;

            end;

          end;

          hence f is left_identity;

          for f1 be morphism of C st f1 |> f holds (f1 (*) f) = f1

          proof

            let f1 be morphism of C;

            assume

             A59: f1 |> f;

            then

            consider y be object such that

             A60: [ [f1, f], y] in the composition of C by XTUPLE_0:def 12;

             [ [f1, f], y] in ((c0 \/ c1) \/ c2) or [ [f1, f], y] in c3 by A60, XBOOLE_0:def 3;

            then

             A61: [ [f1, f], y] in (c0 \/ c1) or [ [f1, f], y] in c2 or [ [f1, f], y] in c3 by XBOOLE_0:def 3;

            per cases by A61, XBOOLE_0:def 3;

              suppose [ [f1, f], y] in c0;

              then

              consider n1,n2 be Element of NAT such that

               A62: [ [f1, f], y] = [ [ [n1, n2], [n1, n2]], [n1, n2]] & n2 = (n1 + 1);

               [f1, f] = [ [n1, n2], [n1, n2]] & y = [n1, n2] by A62, XTUPLE_0: 1;

              then

               A63: f1 = [n1, n2] & f = [n1, n2] by XTUPLE_0: 1;

              

              thus (f1 (*) f) = (the composition of C . (f1,f)) by A59, Def3

              .= (the composition of C . [f1, f]) by BINOP_1:def 1

              .= f1 by A63, A60, FUNCT_1: 1, A62;

            end;

              suppose [ [f1, f], y] in c1;

              then

              consider n1,n2 be Element of NAT such that

               A64: [ [f1, f], y] = [ [ [n1, n2], n2], n2] & n2 = (n1 + 1);

               [f1, f] = [ [n1, n2], n2] & y = n2 by A64, XTUPLE_0: 1;

              hence thesis by A49, XTUPLE_0: 1;

            end;

              suppose [ [f1, f], y] in c2;

              then

              consider n1,n2 be Element of NAT such that

               A65: [ [f1, f], y] = [ [n1, [n1, n2]], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f1, f] = [n1, [n1, n2]] & y = n1 by A65, XTUPLE_0: 1;

              then

               A66: f1 = n1 & f = [n1, n2] by XTUPLE_0: 1;

              

              thus (f1 (*) f) = (the composition of C . (f1,f)) by A59, Def3

              .= (the composition of C . [f1, f]) by BINOP_1:def 1

              .= f1 by A66, A60, FUNCT_1: 1, A65;

            end;

              suppose [ [f1, f], y] in c3;

              then

              consider n1,n2 be Element of NAT such that

               A67: [ [f1, f], y] = [ [n1, n2], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f1, f] = [n1, n2] by A67, XTUPLE_0: 1;

              hence thesis by A49, XTUPLE_0: 1;

            end;

          end;

          hence f is right_identity;

           [ [f, f], f] in c0 by A49;

          then [ [f, f], f] in (c0 \/ c1) by XBOOLE_0:def 3;

          then [ [f, f], f] in ((c0 \/ c1) \/ c2) by XBOOLE_0:def 3;

          then [ [f, f], f] in (((c0 \/ c1) \/ c2) \/ c3) by XBOOLE_0:def 3;

          hence f |> f by FUNCT_1: 1;

        end;

        

         A68: for f1,f2 be morphism of C st f1 in X1 & f1 |> f2 holds (f1 (*) f2) = f1

        proof

          let f1,f2 be morphism of C;

          assume

           A69: f1 in X1;

          reconsider nf1 = f1 as Element of NAT by A69;

          assume

           A70: f1 |> f2;

          per cases by A1, XBOOLE_0:def 3;

            suppose

             A71: f2 in X1;

            reconsider nf2 = f2 as Element of NAT by A71;

            consider y be object such that

             A72: [ [f1, f2], y] in the composition of C by A70, XTUPLE_0:def 12;

             [ [f1, f2], y] in ((c0 \/ c1) \/ c2) or [ [f1, f2], y] in c3 by A72, XBOOLE_0:def 3;

            then

             A73: [ [f1, f2], y] in (c0 \/ c1) or [ [f1, f2], y] in c2 or [ [f1, f2], y] in c3 by XBOOLE_0:def 3;

            per cases by A73, XBOOLE_0:def 3;

              suppose [ [f1, f2], y] in c0;

              then

              consider n1,n2 be Element of NAT such that

               A74: [ [f1, f2], y] = [ [ [n1, n2], [n1, n2]], [n1, n2]] & n2 = (n1 + 1);

               [f1, f2] = [ [n1, n2], [n1, n2]] by A74, XTUPLE_0: 1;

              hence thesis by A71, XTUPLE_0: 1;

            end;

              suppose [ [f1, f2], y] in c1;

              then

              consider n1,n2 be Element of NAT such that

               A75: [ [f1, f2], y] = [ [ [n1, n2], n2], n2] & n2 = (n1 + 1);

               [f1, f2] = [ [n1, n2], n2] & y = n2 by A75, XTUPLE_0: 1;

              hence thesis by A69, XTUPLE_0: 1;

            end;

              suppose [ [f1, f2], y] in c2;

              then

              consider n1,n2 be Element of NAT such that

               A76: [ [f1, f2], y] = [ [n1, [n1, n2]], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f1, f2] = [n1, [n1, n2]] by A76, XTUPLE_0: 1;

              hence thesis by A71, XTUPLE_0: 1;

            end;

              suppose [ [f1, f2], y] in c3;

              then

              consider n1,n2 be Element of NAT such that

               A77: [ [f1, f2], y] = [ [n1, n2], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f1, f2] = [n1, n2] & y = n1 by A77, XTUPLE_0: 1;

              then

               A78: f1 = n1 & f2 = n2 by XTUPLE_0: 1;

              

              thus (f1 (*) f2) = (the composition of C . (f1,f2)) by A70, Def3

              .= (the composition of C . [f1, f2]) by BINOP_1:def 1

              .= f1 by A78, A72, FUNCT_1: 1, A77;

            end;

          end;

            suppose f2 in X2;

            then f2 is right_identity by A48;

            hence thesis by A70;

          end;

        end;

        ex f,f1,f2 be morphism of C st f1 |> f2 & not ((f1 (*) f2) |> f iff f2 |> f)

        proof

          reconsider f1 = 1, f2 = 2, f = 3 as morphism of C by A41;

          take f, f1, f2;

          

           A79: 2 = (1 + 1);

          hence f1 |> f2 by A42;

          

           A80: not f1 |> f

          proof

            assume f1 |> f;

            then

            consider y be object such that

             A81: [ [f1, f], y] in the composition of C by XTUPLE_0:def 12;

             [ [f1, f], y] in ((c0 \/ c1) \/ c2) or [ [f1, f], y] in c3 by A81, XBOOLE_0:def 3;

            then

             A82: [ [f1, f], y] in (c0 \/ c1) or [ [f1, f], y] in c2 or [ [f1, f], y] in c3 by XBOOLE_0:def 3;

            per cases by A82, XBOOLE_0:def 3;

              suppose [ [f1, f], y] in c0;

              then

              consider n1,n2 be Element of NAT such that

               A83: [ [f1, f], y] = [ [ [n1, n2], [n1, n2]], [n1, n2]] & n2 = (n1 + 1);

               [f1, f] = [ [n1, n2], [n1, n2]] by A83, XTUPLE_0: 1;

              hence contradiction by XTUPLE_0: 1;

            end;

              suppose [ [f1, f], y] in c1;

              then

              consider n1,n2 be Element of NAT such that

               A84: [ [f1, f], y] = [ [ [n1, n2], n2], n2] & n2 = (n1 + 1);

               [f1, f] = [ [n1, n2], n2] by A84, XTUPLE_0: 1;

              hence contradiction by XTUPLE_0: 1;

            end;

              suppose [ [f1, f], y] in c2;

              then

              consider n1,n2 be Element of NAT such that

               A85: [ [f1, f], y] = [ [n1, [n1, n2]], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f1, f] = [n1, [n1, n2]] by A85, XTUPLE_0: 1;

              hence contradiction by XTUPLE_0: 1;

            end;

              suppose [ [f1, f], y] in c3;

              then

              consider n1,n2 be Element of NAT such that

               A86: [ [f1, f], y] = [ [n1, n2], n1] & n2 = (n1 + 1) & n1 <> 0 ;

               [f1, f] = [n1, n2] by A86, XTUPLE_0: 1;

              then f1 = n1 & f = n2 by XTUPLE_0: 1;

              hence contradiction by A86;

            end;

          end;

          3 = (2 + 1);

          hence thesis by A42, A80, A79;

        end;

        then

         A87: C is non left_composable;

        for f,f1,f2 be morphism of C st f1 |> f2 holds f |> (f1 (*) f2) iff f |> f1

        proof

          let f,f1,f2 be morphism of C;

          assume

           A88: f1 |> f2;

          per cases by A1, XBOOLE_0:def 3;

            suppose

             A89: f2 in X1;

            per cases by A1, XBOOLE_0:def 3;

              suppose f1 in X1;

              hence thesis by A88, A68;

            end;

              suppose

               A90: f1 in X2;

              then

               A91: f1 is left_identity by A48;

              then

               A92: (f1 (*) f2) = f2 by A88;

              consider n1,n2 be Element of NAT such that

               A93: f1 = [n1, n2] & n2 = (n1 + 1) by A90;

              reconsider n3 = f2 as Element of NAT by A89;

              

               A94: n2 = n3

              proof

                assume

                 A95: n2 <> n3;

                consider y be object such that

                 A96: [ [f1, f2], y] in the composition of C by A88, XTUPLE_0:def 12;

                 [ [f1, f2], y] in ((c0 \/ c1) \/ c2) or [ [f1, f2], y] in c3 by A96, XBOOLE_0:def 3;

                then

                 A97: [ [f1, f2], y] in (c0 \/ c1) or [ [f1, f2], y] in c2 or [ [f1, f2], y] in c3 by XBOOLE_0:def 3;

                per cases by A97, XBOOLE_0:def 3;

                  suppose [ [f1, f2], y] in c0;

                  then

                  consider n1,n2 be Element of NAT such that

                   A98: [ [f1, f2], y] = [ [ [n1, n2], [n1, n2]], [n1, n2]] & n2 = (n1 + 1);

                   [f1, f2] = [ [n1, n2], [n1, n2]] by A98, XTUPLE_0: 1;

                  hence contradiction by XTUPLE_0: 1, A89;

                end;

                  suppose [ [f1, f2], y] in c1;

                  then

                  consider n11,n22 be Element of NAT such that

                   A99: [ [f1, f2], y] = [ [ [n11, n22], n22], n22] & n22 = (n11 + 1);

                   [f1, f2] = [ [n11, n22], n22] by A99, XTUPLE_0: 1;

                  then f1 = [n11, n22] & f2 = n22 by XTUPLE_0: 1;

                  hence contradiction by A95, A93, XTUPLE_0: 1;

                end;

                  suppose [ [f1, f2], y] in c2;

                  then

                  consider n1,n2 be Element of NAT such that

                   A100: [ [f1, f2], y] = [ [n1, [n1, n2]], n1] & n2 = (n1 + 1) & n1 <> 0 ;

                   [f1, f2] = [n1, [n1, n2]] by A100, XTUPLE_0: 1;

                  hence contradiction by XTUPLE_0: 1, A89;

                end;

                  suppose [ [f1, f2], y] in c3;

                  then

                  consider n1,n2 be Element of NAT such that

                   A101: [ [f1, f2], y] = [ [n1, n2], n1] & n2 = (n1 + 1) & n1 <> 0 ;

                   [f1, f2] = [n1, n2] by A101, XTUPLE_0: 1;

                  hence contradiction by A93, XTUPLE_0: 1;

                end;

              end;

              hereby

                assume f |> (f1 (*) f2);

                then

                consider y be object such that

                 A102: [ [f, f2], y] in the composition of C by A92, XTUPLE_0:def 12;

                 [ [f, f2], y] in ((c0 \/ c1) \/ c2) or [ [f, f2], y] in c3 by A102, XBOOLE_0:def 3;

                then

                 A103: [ [f, f2], y] in (c0 \/ c1) or [ [f, f2], y] in c2 or [ [f, f2], y] in c3 by XBOOLE_0:def 3;

                per cases by A103, XBOOLE_0:def 3;

                  suppose [ [f, f2], y] in c0;

                  then

                  consider n,n2 be Element of NAT such that

                   A104: [ [f, f2], y] = [ [ [n, n2], [n, n2]], [n, n2]] & n2 = (n + 1);

                   [f, f2] = [ [n, n2], [n, n2]] by A104, XTUPLE_0: 1;

                  hence f |> f1 by XTUPLE_0: 1, A89;

                end;

                  suppose [ [f, f2], y] in c1;

                  then

                  consider n,n22 be Element of NAT such that

                   A105: [ [f, f2], y] = [ [ [n, n22], n22], n22] & n22 = (n + 1);

                   [f, f2] = [ [n, n22], n22] by A105, XTUPLE_0: 1;

                  then

                   A106: f = [n, n22] & f2 = n22 by XTUPLE_0: 1;

                   [ [f1, f1], f1] in c0 by A93;

                  then [ [f1, f1], f1] in (c0 \/ c1) by XBOOLE_0:def 3;

                  then [ [f1, f1], f1] in ((c0 \/ c1) \/ c2) by XBOOLE_0:def 3;

                  then [ [f1, f1], f1] in the composition of C by XBOOLE_0:def 3;

                  hence f |> f1 by A93, A106, A105, A94, XTUPLE_0:def 12;

                end;

                  suppose [ [f, f2], y] in c2;

                  then

                  consider n,n2 be Element of NAT such that

                   A107: [ [f, f2], y] = [ [n, [n, n2]], n] & n2 = (n + 1) & n <> 0 ;

                   [f, f2] = [n, [n, n2]] by A107, XTUPLE_0: 1;

                  hence f |> f1 by A89, XTUPLE_0: 1;

                end;

                  suppose [ [f, f2], y] in c3;

                  then

                  consider n,n22 be Element of NAT such that

                   A108: [ [f, f2], y] = [ [n, n22], n] & n22 = (n + 1) & n <> 0 ;

                  

                   A109: [f, f2] = [n, n22] by A108, XTUPLE_0: 1;

                  then

                   A110: f = n & f2 = n22 by XTUPLE_0: 1;

                  

                   A111: (n + 1) = (n1 + 1) by A94, A108, A93, A109, XTUPLE_0: 1;

                   [ [n1, [n1, n2]], n1] in c2 by A93, A108, A111;

                  then [ [f, f1], f] in ((c0 \/ c1) \/ c2) by A93, A110, XBOOLE_0:def 3, A94, A108;

                  then [ [f, f1], f] in the composition of C by XBOOLE_0:def 3;

                  hence f |> f1 by XTUPLE_0:def 12;

                end;

              end;

              assume

               A112: f |> f1;

              f |> f2

              proof

                consider y be object such that

                 A113: [ [f, f1], y] in the composition of C by A112, XTUPLE_0:def 12;

                 [ [f, f1], y] in ((c0 \/ c1) \/ c2) or [ [f, f1], y] in c3 by A113, XBOOLE_0:def 3;

                then

                 A114: [ [f, f1], y] in (c0 \/ c1) or [ [f, f1], y] in c2 or [ [f, f1], y] in c3 by XBOOLE_0:def 3;

                per cases by A114, XBOOLE_0:def 3;

                  suppose [ [f, f1], y] in c0;

                  then

                  consider n,n1 be Element of NAT such that

                   A115: [ [f, f1], y] = [ [ [n, n1], [n, n1]], [n, n1]] & n1 = (n + 1);

                   [f, f1] = [ [n, n1], [n, n1]] by A115, XTUPLE_0: 1;

                  then f = [n, n1] & f1 = [n, n1] by XTUPLE_0: 1;

                  hence f |> f2 by A88;

                end;

                  suppose [ [f, f1], y] in c1;

                  then

                  consider n,n1 be Element of NAT such that

                   A116: [ [f, f1], y] = [ [ [n, n1], n1], n1] & n1 = (n + 1);

                   [f, f1] = [ [n, n1], n1] by A116, XTUPLE_0: 1;

                  hence f |> f2 by A93, XTUPLE_0: 1;

                end;

                  suppose [ [f, f1], y] in c2;

                  then

                  consider n,n11 be Element of NAT such that

                   A117: [ [f, f1], y] = [ [n, [n, n11]], n] & n11 = (n + 1) & n <> 0 ;

                   [f, f1] = [n, [n, n11]] by A117, XTUPLE_0: 1;

                  then

                   A118: f = n & f1 = [n, n11] by XTUPLE_0: 1;

                  then

                   A119: n = n1 & n11 = n2 by A93, XTUPLE_0: 1;

                   [ [n1, n2], n1] in c3 by A117, A119;

                  then [ [f, f2], f] in the composition of C by A119, A118, A94, XBOOLE_0:def 3;

                  hence f |> f2 by XTUPLE_0:def 12;

                end;

                  suppose [ [f, f1], y] in c3;

                  then

                  consider n,n1 be Element of NAT such that

                   A120: [ [f, f1], y] = [ [n, n1], n] & n1 = (n + 1) & n <> 0 ;

                   [f, f1] = [n, n1] by A120, XTUPLE_0: 1;

                  hence f |> f2 by A93, XTUPLE_0: 1;

                end;

              end;

              hence f |> (f1 (*) f2) by A91, A88;

            end;

          end;

            suppose f2 in X2;

            then f2 is right_identity by A48;

            hence thesis by A88;

          end;

        end;

        then

         A121: C is right_composable;

        for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f |> f1 & f is left_identity

        proof

          let f1 be morphism of C;

          assume

           A122: f1 in the carrier of C;

          per cases by A122, XBOOLE_0:def 3;

            suppose

             A123: f1 in X1;

            then

             A124: f1 in NAT & not f1 in { 0 } by XBOOLE_0:def 5;

            reconsider n2 = f1 as Element of NAT by A123;

            reconsider n22 = n2 as Nat;

            n22 <> 0 by A124, TARSKI:def 1;

            then

            consider n11 be Nat such that

             A125: n22 = (n11 + 1) by NAT_1: 6;

            reconsider n1 = n11 as Element of NAT by ORDINAL1:def 12;

            

             A126: [n1, n2] in X2 by A125;

            then

            reconsider f = [n1, n2] as morphism of C by XBOOLE_0:def 3;

            take f;

             [ [ [n1, n2], n2], n2] in c1 by A125;

            then [ [f, f1], f1] in (c0 \/ c1) by XBOOLE_0:def 3;

            then [ [f, f1], f1] in ((c0 \/ c1) \/ c2) by XBOOLE_0:def 3;

            then [ [f, f1], f1] in the composition of C by XBOOLE_0:def 3;

            hence f |> f1 by XTUPLE_0:def 12;

            thus f is left_identity by A126, A48;

          end;

            suppose

             A127: f1 in X2;

            set f = f1;

            take f;

            thus thesis by A127, A48;

          end;

        end;

        then

         A128: C is with_left_identities;

        for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f1 |> f & f is right_identity

        proof

          let f1 be morphism of C;

          assume

           A129: f1 in the carrier of C;

          per cases by A129, XBOOLE_0:def 3;

            suppose

             A130: f1 in X1;

            then

             A131: f1 in NAT & not f1 in { 0 } by XBOOLE_0:def 5;

            reconsider n1 = f1 as Element of NAT by A130;

            

             A132: n1 <> 0 by A131, TARSKI:def 1;

            reconsider n2 = (n1 + 1) as Element of NAT by ORDINAL1:def 12;

            

             A133: [n1, n2] in X2;

            then

            reconsider f = [n1, n2] as morphism of C by XBOOLE_0:def 3;

            take f;

             [ [n1, [n1, n2]], n1] in c2 by A132;

            then [ [f1, f], f1] in ((c0 \/ c1) \/ c2) by XBOOLE_0:def 3;

            then [ [f1, f], f1] in the composition of C by XBOOLE_0:def 3;

            hence f1 |> f by XTUPLE_0:def 12;

            thus f is right_identity by A133, A48;

          end;

            suppose

             A134: f1 in X2;

            set f = f1;

            take f;

            thus thesis by A134, A48;

          end;

        end;

        then

         A135: C is with_identities by A128, Def7;

        for f1,f2,f3 be morphism of C st f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) holds (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3)

        proof

          let f1,f2,f3 be morphism of C;

          assume

           A136: f1 |> f2;

          assume f2 |> f3;

          assume

           A137: (f1 (*) f2) |> f3;

          assume

           A138: f1 |> (f2 (*) f3);

          

           A139: C is non empty by A136;

          per cases by A139, XBOOLE_0:def 3;

            suppose

             A140: f1 in X1;

            then

             A141: (f1 (*) (f2 (*) f3)) = f1 & (f1 (*) f2) = f1 by A136, A138, A68;

            thus (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3) by A140, A68, A141, A137;

          end;

            suppose f1 in X2;

            then f1 is left_identity by A48;

            then (f1 (*) (f2 (*) f3)) = (f2 (*) f3) & (f1 (*) f2) = f2 by A136, A138;

            hence (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3);

          end;

        end;

        hence thesis by A87, A121, A135, Def10;

      end;

    end

    registration

      cluster left_composable non right_composable with_identities associative for CategoryStr;

      correctness

      proof

        set C1 = the non left_composable right_composable with_identities associative CategoryStr;

        set C = (C1 opp );

        take C;

        thus C is left_composable by Th5;

        thus C is non right_composable by Th4;

        thus C is with_identities by Th6, Th7, Def12;

        thus thesis by Th8;

      end;

    end

    registration

      cluster non associative composable with_identities for CategoryStr;

      correctness

      proof

        set X = NAT ;

        set comp = { [ [n1, n2], n3] where n1,n2,n3 be Element of NAT : (n1 <> n2 implies n3 = (n1 + n2)) & (n1 = n2 implies n3 = 0 ) };

        

         A1: for x,y1,y2 be object st [x, y1] in comp & [x, y2] in comp holds y1 = y2

        proof

          let x,y1,y2 be object;

          assume [x, y1] in comp;

          then

          consider n11,n12,n13 be Element of NAT such that

           A2: [x, y1] = [ [n11, n12], n13] & (n11 <> n12 implies n13 = (n11 + n12)) & (n11 = n12 implies n13 = 0 );

          assume [x, y2] in comp;

          then

          consider n21,n22,n23 be Element of NAT such that

           A3: [x, y2] = [ [n21, n22], n23] & (n21 <> n22 implies n23 = (n21 + n22)) & (n21 = n22 implies n23 = 0 );

          

           A4: x = [n11, n12] & y1 = n13 by A2, XTUPLE_0: 1;

          x = [n21, n22] & y2 = n23 by A3, XTUPLE_0: 1;

          then

           A5: n11 = n21 & n12 = n22 by A4, XTUPLE_0: 1;

          per cases ;

            suppose n11 <> n12;

            thus y1 = y2 by A2, A3, A5, XTUPLE_0: 1;

          end;

            suppose n11 = n12;

            thus y1 = y2 by A2, A3, A5, XTUPLE_0: 1;

          end;

        end;

        for x be object st x in comp holds x in [: [:X, X:], X:]

        proof

          let x be object;

          assume x in comp;

          then

          consider n11,n12,n13 be Element of NAT such that

           A6: x = [ [n11, n12], n13] & (n11 <> n12 implies n13 = (n11 + n12)) & (n11 = n12 implies n13 = 0 );

           [n11, n12] in [:X, X:] by ZFMISC_1:def 2;

          hence thesis by A6, ZFMISC_1:def 2;

        end;

        then

        reconsider comp as PartFunc of [:X, X:], X by A1, TARSKI:def 3, FUNCT_1:def 1;

        set C = CategoryStr (# X, comp #);

        

         A7: for f1,f2 be morphism of C holds f1 |> f2

        proof

          let f1,f2 be morphism of C;

          reconsider n1 = f1, n2 = f2 as Element of NAT ;

          per cases ;

            suppose

             A8: n1 <> n2;

            reconsider n3 = (n1 + n2) as Element of NAT by ORDINAL1:def 12;

             [ [n1, n2], n3] in the composition of C by A8;

            hence thesis by FUNCT_1: 1;

          end;

            suppose

             A9: n1 = n2;

            set n3 = 0 ;

             [ [n1, n2], n3] in the composition of C by A9;

            hence thesis by FUNCT_1: 1;

          end;

        end;

        

         A10: for f1,f2 be morphism of C st f1 = 0 holds (f1 (*) f2) = f2 & (f2 (*) f1) = f2

        proof

          let f1,f2 be morphism of C;

          assume

           A11: f1 = 0 ;

          reconsider n2 = f2 as Element of NAT ;

           [f1, f2] in ( dom the composition of C) by A7, Def2;

          then

          consider y be object such that

           A12: [ [f1, f2], y] in the composition of C by XTUPLE_0:def 12;

          consider n1,n2,n3 be Element of NAT such that

           A13: [ [f1, f2], y] = [ [n1, n2], n3] & (n1 <> n2 implies n3 = (n1 + n2)) & (n1 = n2 implies n3 = 0 ) by A12;

           [f1, f2] = [n1, n2] & y = n3 by A13, XTUPLE_0: 1;

          then

           A14: f1 = n1 & f2 = n2 by XTUPLE_0: 1;

          

          thus (f1 (*) f2) = (the composition of C . (f1,f2)) by Def3, A7

          .= (the composition of C . [f1, f2]) by BINOP_1:def 1

          .= f2 by FUNCT_1: 1, A12, A13, A14, A11;

           [f2, f1] in ( dom the composition of C) by A7, Def2;

          then

          consider y be object such that

           A15: [ [f2, f1], y] in the composition of C by XTUPLE_0:def 12;

          consider n2,n1,n3 be Element of NAT such that

           A16: [ [f2, f1], y] = [ [n2, n1], n3] & (n2 <> n1 implies n3 = (n2 + n1)) & (n2 = n1 implies n3 = 0 ) by A15;

           [f2, f1] = [n2, n1] & y = n3 by A16, XTUPLE_0: 1;

          then

           A17: f2 = n2 & f1 = n1 by XTUPLE_0: 1;

          

          thus (f2 (*) f1) = (the composition of C . (f2,f1)) by Def3, A7

          .= (the composition of C . [f2, f1]) by BINOP_1:def 1

          .= f2 by FUNCT_1: 1, A15, A16, A17, A11;

        end;

        

         A18: C is left_composable by A7;

        for f,f1,f2 be morphism of C st f1 |> f2 holds f |> (f1 (*) f2) iff f |> f1 by A7;

        then

         A19: C is composable by A18, Def9;

        for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f |> f1 & f is left_identity

        proof

          let f1 be morphism of C;

          assume f1 in the carrier of C;

          reconsider f = 0 as morphism of C;

          take f;

          thus f |> f1 by A7;

          thus f is left_identity by A10;

        end;

        then

         A20: C is with_left_identities;

        for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f1 |> f & f is right_identity

        proof

          let f1 be morphism of C;

          assume f1 in the carrier of C;

          reconsider f = 0 as morphism of C;

          take f;

          thus f1 |> f by A7;

          thus f is right_identity by A10;

        end;

        then

         A21: C is with_identities by A20, Def7;

        

         A22: for f1,f2 be morphism of C, n1,n2 be Element of NAT st f1 = n1 & f2 = n2 & n1 = n2 holds (f1 (*) f2) = 0

        proof

          let f1,f2 be morphism of C;

          let n1,n2 be Element of NAT ;

          assume

           A23: f1 = n1 & f2 = n2;

          assume

           A24: n1 = n2;

           [f1, f2] in ( dom the composition of C) by A7, Def2;

          then

          consider y be object such that

           A25: [ [f1, f2], y] in the composition of C by XTUPLE_0:def 12;

          consider n11,n22,n33 be Element of NAT such that

           A26: [ [f1, f2], y] = [ [n11, n22], n33] & (n11 <> n22 implies n33 = (n11 + n22)) & (n11 = n22 implies n33 = 0 ) by A25;

           [f1, f2] = [n11, n22] & y = n33 by A26, XTUPLE_0: 1;

          then

           A27: f1 = n11 & f2 = n22 by XTUPLE_0: 1;

          

          thus (f1 (*) f2) = (the composition of C . (f1,f2)) by Def3, A7

          .= (the composition of C . [f1, f2]) by BINOP_1:def 1

          .= 0 by A27, FUNCT_1: 1, A25, A26, A24, A23;

        end;

        

         A28: for f1,f2 be morphism of C, n1,n2 be Element of NAT st f1 = n1 & f2 = n2 & n1 <> n2 holds (f1 (*) f2) = (n1 + n2)

        proof

          let f1,f2 be morphism of C;

          let n1,n2 be Element of NAT ;

          assume

           A29: f1 = n1 & f2 = n2;

          assume

           A30: n1 <> n2;

           [f1, f2] in ( dom the composition of C) by A7, Def2;

          then

          consider y be object such that

           A31: [ [f1, f2], y] in the composition of C by XTUPLE_0:def 12;

          consider n11,n22,n33 be Element of NAT such that

           A32: [ [f1, f2], y] = [ [n11, n22], n33] & (n11 <> n22 implies n33 = (n11 + n22)) & (n11 = n22 implies n33 = 0 ) by A31;

           [f1, f2] = [n11, n22] & y = n33 by A32, XTUPLE_0: 1;

          then

           A33: f1 = n11 & f2 = n22 by XTUPLE_0: 1;

          

          thus (f1 (*) f2) = (the composition of C . (f1,f2)) by Def3, A7

          .= (the composition of C . [f1, f2]) by BINOP_1:def 1

          .= (n1 + n2) by A33, FUNCT_1: 1, A31, A32, A30, A29;

        end;

        ex f1,f2,f3 be morphism of C st f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) & not (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3)

        proof

          reconsider f1 = 1, f2 = 2, f3 = 3 as morphism of C;

          take f1, f2, f3;

          thus f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) by A7;

          

           A34: (f1 (*) f2) = (1 + 2) & (f2 (*) f3) = (2 + 3) by A28;

          reconsider f12 = 3, f23 = 5 as morphism of C;

          (f1 (*) f23) = (1 + 5) & (f12 (*) f3) = 0 by A22, A28;

          hence thesis by A34;

        end;

        hence thesis by A19, A21, Def10;

      end;

    end

    registration

      cluster empty for CategoryStr;

      correctness

      proof

        reconsider X = the empty set as set;

        reconsider F = the PartFunc of [: the empty set, the empty set:], the empty set as PartFunc of [:X, X:], X;

        set C = CategoryStr (# X, F #);

        take C;

        thus thesis;

      end;

    end

    registration

      cluster empty -> left_composable right_composable with_left_identities with_right_identities associative for CategoryStr;

      correctness

      proof

        let C be CategoryStr;

        assume

         A1: C is empty;

        for f,f1,f2 be morphism of C holds f1 |> f2 implies ((f1 (*) f2) |> f iff f2 |> f) by A1;

        hence C is left_composable;

        for f,f1,f2 be morphism of C holds f1 |> f2 implies (f |> (f1 (*) f2) iff f |> f1) by A1;

        hence C is right_composable;

        thus C is with_left_identities by A1;

        thus C is with_right_identities by A1;

        for f1,f2,f3 be morphism of C holds f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) implies (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3) by A1;

        hence thesis;

      end;

    end

    registration

      cluster strict with_left_identities with_right_identities left_composable right_composable associative for CategoryStr;

      correctness

      proof

        set C = ( the empty CategoryStr opp );

        take C;

        thus thesis by Th4, Th5, Th8;

      end;

    end

    registration

      cluster strict with_identities composable associative for CategoryStr;

      correctness

      proof

        set C = the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr;

        take C;

        thus thesis;

      end;

    end

    definition

      mode category is with_identities composable associative CategoryStr;

    end

    definition

      let C, f;

      :: CAT_6:def14

      attr f is identity means f is left_identity right_identity;

    end

    theorem :: CAT_6:9

    

     Th9: C is with_identities implies (f is left_identity iff f is right_identity)

    proof

      assume

       A1: C is with_identities;

      hereby

        assume

         A2: f is left_identity;

        for f1 be morphism of C st f1 |> f holds (f1 (*) f) = f1

        proof

          let f1 be morphism of C;

          assume

           A3: f1 |> f;

          then C is non empty;

          then

          consider g be morphism of C such that

           A4: f |> g & g is right_identity by A1, Def7;

          f = (f (*) g) by A4

          .= g by A2, A4;

          hence (f1 (*) f) = f1 by A4, A3;

        end;

        hence f is right_identity;

      end;

      assume

       A5: f is right_identity;

      for f1 be morphism of C st f |> f1 holds (f (*) f1) = f1

      proof

        let f1 be morphism of C;

        assume

         A6: f |> f1;

        then C is non empty;

        then

        consider g be morphism of C such that

         A7: g |> f & g is left_identity by A1, Def6;

        f = (g (*) f) by A7

        .= g by A5, A7;

        hence (f (*) f1) = f1 by A7, A6;

      end;

      hence f is left_identity;

    end;

    theorem :: CAT_6:10

    

     Th10: C is empty implies f is identity

    proof

      assume C is empty;

      then (for f1 be morphism of C st f |> f1 holds (f (*) f1) = f1) & (for f1 be morphism of C st f1 |> f holds (f1 (*) f) = f1);

      then f is left_identity & f is right_identity;

      hence f is identity;

    end;

    theorem :: CAT_6:11

    

     Th11: for g1,g2 be morphism of the CategoryStr of C st f1 = g1 & f2 = g2 & f1 |> f2 holds (f1 (*) f2) = (g1 (*) g2)

    proof

      let g1,g2 be morphism of the CategoryStr of C;

      assume

       A1: f1 = g1 & f2 = g2;

      assume

       A2: f1 |> f2;

      then

       A3: g1 |> g2 by A1;

      

      thus (f1 (*) f2) = (the composition of C . (f1,f2)) by A2, Def3

      .= (g1 (*) g2) by A1, A3, Def3;

    end;

    theorem :: CAT_6:12

    

     Th12: C is left_composable iff the CategoryStr of C is left_composable

    proof

      hereby

        assume

         A1: C is left_composable;

        for g,g1,g2 be morphism of the CategoryStr of C st g1 |> g2 holds (g1 (*) g2) |> g iff g2 |> g

        proof

          let g,g1,g2 be morphism of the CategoryStr of C;

          reconsider f = g, f1 = g1, f2 = g2 as morphism of C;

          assume g1 |> g2;

          then

           A2: f1 |> f2;

          hereby

            assume (g1 (*) g2) |> g;

            then (f1 (*) f2) |> f by A2, Th11;

            then f2 |> f by A2, A1;

            hence g2 |> g;

          end;

          assume g2 |> g;

          then f2 |> f;

          then (f1 (*) f2) |> f by A2, A1;

          hence (g1 (*) g2) |> g by A2, Th11;

        end;

        hence the CategoryStr of C is left_composable;

      end;

      assume

       A3: the CategoryStr of C is left_composable;

      for f,f1,f2 be morphism of C st f1 |> f2 holds (f1 (*) f2) |> f iff f2 |> f

      proof

        let f,f1,f2 be morphism of C;

        reconsider g = f, g1 = f1, g2 = f2 as morphism of the CategoryStr of C;

        assume

         A4: f1 |> f2;

        then

         A5: g1 |> g2;

        hereby

          assume (f1 (*) f2) |> f;

          then (g1 (*) g2) |> g by A4, Th11;

          then g2 |> g by A3, A5;

          hence f2 |> f;

        end;

        assume f2 |> f;

        then g2 |> g;

        then (g1 (*) g2) |> g by A3, A5;

        hence (f1 (*) f2) |> f by A4, Th11;

      end;

      hence C is left_composable;

    end;

    theorem :: CAT_6:13

    

     Th13: C is right_composable iff the CategoryStr of C is right_composable

    proof

      hereby

        assume

         A1: C is right_composable;

        for g,g1,g2 be morphism of the CategoryStr of C st g1 |> g2 holds g |> (g1 (*) g2) iff g |> g1

        proof

          let g,g1,g2 be morphism of the CategoryStr of C;

          reconsider f = g, f1 = g1, f2 = g2 as morphism of C;

          assume g1 |> g2;

          then

           A2: f1 |> f2;

          hereby

            assume g |> (g1 (*) g2);

            then f |> (f1 (*) f2) by A2, Th11;

            then f |> f1 by A2, A1;

            hence g |> g1;

          end;

          assume g |> g1;

          then f |> f1;

          then f |> (f1 (*) f2) by A2, A1;

          hence g |> (g1 (*) g2) by A2, Th11;

        end;

        hence the CategoryStr of C is right_composable;

      end;

      assume

       A3: the CategoryStr of C is right_composable;

      for f,f1,f2 be morphism of C st f1 |> f2 holds f |> (f1 (*) f2) iff f |> f1

      proof

        let f,f1,f2 be morphism of C;

        reconsider g = f, g1 = f1, g2 = f2 as morphism of the CategoryStr of C;

        assume

         A4: f1 |> f2;

        then

         A5: g1 |> g2;

        hereby

          assume f |> (f1 (*) f2);

          then g |> (g1 (*) g2) by A4, Th11;

          then g |> g1 by A3, A5;

          hence f |> f1;

        end;

        assume f |> f1;

        then g |> g1;

        then g |> (g1 (*) g2) by A3, A5;

        hence f |> (f1 (*) f2) by A4, Th11;

      end;

      hence C is right_composable;

    end;

    theorem :: CAT_6:14

    C is composable iff the CategoryStr of C is composable by Th12, Th13;

    theorem :: CAT_6:15

    C is associative iff the CategoryStr of C is associative

    proof

      hereby

        assume

         A1: C is associative;

        for g1,g2,g3 be morphism of the CategoryStr of C st g1 |> g2 & g2 |> g3 & (g1 (*) g2) |> g3 & g1 |> (g2 (*) g3) holds (g1 (*) (g2 (*) g3)) = ((g1 (*) g2) (*) g3)

        proof

          let g1,g2,g3 be morphism of the CategoryStr of C;

          reconsider f1 = g1, f2 = g2, f3 = g3 as morphism of C;

          assume g1 |> g2 & g2 |> g3;

          then

           A2: f1 |> f2 & f2 |> f3;

          

           A3: (f1 (*) f2) = (g1 (*) g2) & (f2 (*) f3) = (g2 (*) g3) by A2, Th11;

          assume (g1 (*) g2) |> g3 & g1 |> (g2 (*) g3);

          then

           A4: (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) by A2, Th11;

          then (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3) by A2, A1;

          

          hence (g1 (*) (g2 (*) g3)) = ((f1 (*) f2) (*) f3) by A4, A3, Th11

          .= ((g1 (*) g2) (*) g3) by A4, A3, Th11;

        end;

        hence the CategoryStr of C is associative;

      end;

      assume

       A5: the CategoryStr of C is associative;

      for f1,f2,f3 be morphism of C st f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) holds (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3)

      proof

        let f1,f2,f3 be morphism of C;

        reconsider g1 = f1, g2 = f2, g3 = f3 as morphism of the CategoryStr of C;

        assume

         A6: f1 |> f2 & f2 |> f3;

        then

         A7: g1 |> g2 & g2 |> g3;

        

         A8: (f1 (*) f2) = (g1 (*) g2) & (f2 (*) f3) = (g2 (*) g3) by A6, Th11;

        assume

         A9: (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3);

        then (g1 (*) g2) |> g3 & g1 |> (g2 (*) g3) by A6, Th11;

        then (g1 (*) (g2 (*) g3)) = ((g1 (*) g2) (*) g3) by A7, A5;

        

        hence (f1 (*) (f2 (*) f3)) = ((g1 (*) g2) (*) g3) by A9, A8, Th11

        .= ((f1 (*) f2) (*) f3) by A9, A8, Th11;

      end;

      hence C is associative;

    end;

    theorem :: CAT_6:16

    

     Th16: for g be morphism of the CategoryStr of C st f = g holds f is left_identity iff g is left_identity

    proof

      let g be morphism of the CategoryStr of C;

      assume

       A1: f = g;

      hereby

        assume

         A2: f is left_identity;

        for g1 be morphism of the CategoryStr of C st g |> g1 holds (g (*) g1) = g1

        proof

          let g1 be morphism of the CategoryStr of C;

          reconsider f1 = g1 as morphism of C;

          assume g |> g1;

          then

           A3: f |> f1 by A1;

          then (f (*) f1) = f1 by A2;

          hence (g (*) g1) = g1 by A1, A3, Th11;

        end;

        hence g is left_identity;

      end;

      assume

       A4: g is left_identity;

      for f2 be morphism of C st f |> f2 holds (f (*) f2) = f2

      proof

        let f2 be morphism of C;

        reconsider g2 = f2 as morphism of the CategoryStr of C;

        assume

         A5: f |> f2;

        then g |> g2 by A1;

        then (g (*) g2) = g2 by A4;

        hence (f (*) f2) = f2 by A1, A5, Th11;

      end;

      hence f is left_identity;

    end;

    theorem :: CAT_6:17

    

     Th17: C is with_left_identities iff the CategoryStr of C is with_left_identities

    proof

      hereby

        assume

         A1: C is with_left_identities;

        for g1 be morphism of the CategoryStr of C st g1 in the carrier of the CategoryStr of C holds ex g be morphism of the CategoryStr of C st g |> g1 & g is left_identity

        proof

          let g1 be morphism of the CategoryStr of C;

          reconsider f1 = g1 as morphism of C;

          assume g1 in the carrier of the CategoryStr of C;

          then

          consider f be morphism of C such that

           A2: f |> f1 & f is left_identity by A1;

          reconsider g = f as morphism of the CategoryStr of C;

          take g;

          thus g |> g1 by A2;

          thus g is left_identity by A2, Th16;

        end;

        hence the CategoryStr of C is with_left_identities;

      end;

      assume

       A3: the CategoryStr of C is with_left_identities;

      for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f |> f1 & f is left_identity

      proof

        let f1 be morphism of C;

        reconsider g1 = f1 as morphism of the CategoryStr of C;

        assume f1 in the carrier of C;

        then

        consider g be morphism of the CategoryStr of C such that

         A4: g |> g1 & g is left_identity by A3;

        reconsider f = g as morphism of C;

        take f;

        thus f |> f1 by A4;

        thus f is left_identity by A4, Th16;

      end;

      hence C is with_left_identities;

    end;

    theorem :: CAT_6:18

    

     Th18: for g be morphism of the CategoryStr of C st f = g holds f is right_identity iff g is right_identity

    proof

      let g be morphism of the CategoryStr of C;

      assume

       A1: f = g;

      hereby

        assume

         A2: f is right_identity;

        for g1 be morphism of the CategoryStr of C st g1 |> g holds (g1 (*) g) = g1

        proof

          let g1 be morphism of the CategoryStr of C;

          reconsider f1 = g1 as morphism of C;

          assume g1 |> g;

          then

           A3: f1 |> f by A1;

          then (f1 (*) f) = f1 by A2;

          hence (g1 (*) g) = g1 by A1, A3, Th11;

        end;

        hence g is right_identity;

      end;

      assume

       A4: g is right_identity;

      for f1 be morphism of C st f1 |> f holds (f1 (*) f) = f1

      proof

        let f1 be morphism of C;

        reconsider g1 = f1 as morphism of the CategoryStr of C;

        assume

         A5: f1 |> f;

        then g1 |> g by A1;

        then (g1 (*) g) = g1 by A4;

        hence (f1 (*) f) = f1 by A1, A5, Th11;

      end;

      hence f is right_identity;

    end;

    theorem :: CAT_6:19

    

     Th19: C is with_right_identities iff the CategoryStr of C is with_right_identities

    proof

      hereby

        assume

         A1: C is with_right_identities;

        for g1 be morphism of the CategoryStr of C st g1 in the carrier of the CategoryStr of C holds ex g be morphism of the CategoryStr of C st g1 |> g & g is right_identity

        proof

          let g1 be morphism of the CategoryStr of C;

          reconsider f1 = g1 as morphism of C;

          assume g1 in the carrier of the CategoryStr of C;

          then

          consider f be morphism of C such that

           A2: f1 |> f & f is right_identity by A1;

          reconsider g = f as morphism of the CategoryStr of C;

          take g;

          thus g1 |> g by A2;

          thus g is right_identity by A2, Th18;

        end;

        hence the CategoryStr of C is with_right_identities;

      end;

      assume

       A3: the CategoryStr of C is with_right_identities;

      for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f1 |> f & f is right_identity

      proof

        let f1 be morphism of C;

        reconsider g1 = f1 as morphism of the CategoryStr of C;

        assume f1 in the carrier of C;

        then

        consider g be morphism of the CategoryStr of C such that

         A4: g1 |> g & g is right_identity by A3;

        reconsider f = g as morphism of C;

        take f;

        thus f1 |> f by A4;

        thus f is right_identity by A4, Th18;

      end;

      hence C is with_right_identities;

    end;

    theorem :: CAT_6:20

    C is with_identities iff the CategoryStr of C is with_identities by Th17, Th19;

    definition

      let C;

      :: CAT_6:def15

      attr C is discrete means

      : Def15: for f be morphism of C holds f is identity;

    end

    

     Lm1: ( the empty CategoryStr opp ) is discrete

    proof

      set C = ( the empty CategoryStr opp );

      for f be morphism of C holds f is identity

      proof

        let f be morphism of C;

        for f1 be morphism of C st f |> f1 holds (f (*) f1) = f1;

        then

         A1: f is left_identity;

        for f1 be morphism of C st f1 |> f holds (f1 (*) f) = f1;

        hence f is identity by A1, Def5;

      end;

      hence thesis;

    end;

    registration

      cluster strict empty discrete with_identities composable associative for CategoryStr;

      correctness

      proof

        set C = ( the empty CategoryStr opp );

        take C;

        C is left_composable right_composable with_left_identities with_right_identities associative by Th4, Th5, Th8;

        hence thesis by Lm1;

      end;

    end

    theorem :: CAT_6:21

    

     Th21: for C be discrete CategoryStr, f1,f2 be morphism of C st f1 |> f2 holds f1 = f2 & (f1 (*) f2) = f2

    proof

      let C be discrete CategoryStr;

      let f1,f2 be morphism of C;

      assume

       A1: f1 |> f2;

      f2 is identity by Def15;

      then

       A2: (f1 (*) f2) = f1 by Def5, A1;

      f1 is identity by Def15;

      hence thesis by A2, A1, Def4;

    end;

    registration

      cluster discrete -> composable associative for CategoryStr;

      correctness

      proof

        let C be CategoryStr;

        assume

         A1: C is discrete;

        

         A2: for f,g,h be morphism of C holds ((h (*) g) |> f & h |> g implies g |> f) & (h |> (g (*) f) & g |> f implies h |> g) & (g |> f & h |> g implies (h (*) g) |> f & h |> (g (*) f))

        proof

          let f,g,h be morphism of C;

          thus (h (*) g) |> f & h |> g implies g |> f by A1, Th21;

          thus h |> (g (*) f) & g |> f implies h |> g

          proof

            assume

             A3: h |> (g (*) f) & g |> f;

            then (g (*) f) = f & f = g by A1, Th21;

            hence h |> g by A3;

          end;

          assume

           A4: g |> f;

          assume

           A5: h |> g;

          thus (h (*) g) |> f by A4, A5, A1, Th21;

          g |> (g (*) f) & h = g by A4, A5, A1, Th21;

          hence h |> (g (*) f);

        end;

        

         A6: for f,g,h be morphism of C st h |> g & g |> f holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

        proof

          let f,g,h be morphism of C;

          assume

           A7: h |> g;

          assume g |> f;

          then

           A8: f = g & (g (*) f) = f by A1, Th21;

          

          thus (h (*) (g (*) f)) = g by A1, Th21, A7, A8

          .= ((h (*) g) (*) f) by A1, Th21, A7, A8;

        end;

        

         A9: C is left_composable by A2;

        for f,f1,f2 be morphism of C holds f1 |> f2 implies (f |> (f1 (*) f2) iff f |> f1) by A2;

        hence thesis by A6, A9, Def9;

      end;

    end

    definition

      let X be set;

      :: CAT_6:def16

      func DiscreteCat (X) -> strict discrete category means

      : Def16: the carrier of it = X;

      existence

      proof

        per cases ;

          suppose

           A1: X is empty;

          set C = the strict empty discrete with_identities composable associative CategoryStr;

          take C;

          thus thesis by A1;

        end;

          suppose not X is empty;

          set F = { [ [x, x], x] where x be Element of X : x in X };

          

           A2: for x,y1,y2 be object st [x, y1] in F & [x, y2] in F holds y1 = y2

          proof

            let x,y1,y2 be object;

            assume [x, y1] in F;

            then

            consider x1 be Element of X such that

             A3: [x, y1] = [ [x1, x1], x1] & x1 in X;

            assume [x, y2] in F;

            then

            consider x2 be Element of X such that

             A4: [x, y2] = [ [x2, x2], x2] & x2 in X;

            

             A5: x = [x1, x1] & y1 = x1 by A3, XTUPLE_0: 1;

            x = [x2, x2] & y2 = x2 by A4, XTUPLE_0: 1;

            hence y1 = y2 by A5, XTUPLE_0: 1;

          end;

          for x be object st x in F holds x in [: [:X, X:], X:]

          proof

            let x be object;

            assume x in F;

            then

            consider x1 be Element of X such that

             A6: x = [ [x1, x1], x1] & x1 in X;

             [x1, x1] in [:X, X:] by A6, ZFMISC_1: 87;

            hence x in [: [:X, X:], X:] by A6, ZFMISC_1: 87;

          end;

          then

          reconsider F as PartFunc of [:X, X:], X by A2, TARSKI:def 3, FUNCT_1:def 1;

          set C = CategoryStr (# X, F #);

          for u be morphism of C holds u is identity

          proof

            let u be morphism of C;

            

             A7: for f be morphism of C st u |> f holds (u (*) f) = f

            proof

              let f be morphism of C;

              assume

               A8: u |> f;

              (u (*) f) = (F . (u,f)) by A8, Def3

              .= (F . [u, f]) by BINOP_1:def 1;

              then [ [u, f], (u (*) f)] in F by A8, FUNCT_1:def 2;

              then

              consider x be Element of X such that

               A9: [ [u, f], (u (*) f)] = [ [x, x], x] & x in X;

               [u, f] = [x, x] & (u (*) f) = x by A9, XTUPLE_0: 1;

              hence (u (*) f) = f by XTUPLE_0: 1;

            end;

            for g be morphism of C st g |> u holds (g (*) u) = g

            proof

              let g be morphism of C;

              assume

               A10: g |> u;

              (g (*) u) = (F . (g,u)) by A10, Def3

              .= (F . [g, u]) by BINOP_1:def 1;

              then [ [g, u], (g (*) u)] in F by A10, FUNCT_1:def 2;

              then

              consider x be Element of X such that

               A11: [ [g, u], (g (*) u)] = [ [x, x], x] & x in X;

               [g, u] = [x, x] & (g (*) u) = x by A11, XTUPLE_0: 1;

              hence (g (*) u) = g by XTUPLE_0: 1;

            end;

            then u is left_identity & u is right_identity by A7;

            hence u is identity;

          end;

          then

          reconsider C as strict discrete CategoryStr by Def15;

           A12:

          now

            let f be morphism of C;

            assume

             A13: f in the carrier of C;

            then

             A14: f is identity & f in X by Def15;

            reconsider x = f as Element of X;

             [ [f, f], f] in { [ [x, x], x] where x be Element of X : x in X } by A13;

            then [f, f] in ( dom the composition of C) by XTUPLE_0:def 12;

            hence (ex c be morphism of C st c |> f & c is left_identity) & (ex d be morphism of C st f |> d & d is right_identity) by Def2, A14;

          end;

          C is with_left_identities & C is with_right_identities by A12;

          then

          reconsider C as strict discrete composable associative with_identities CategoryStr by Def12;

          take C;

          thus thesis;

        end;

      end;

      uniqueness

      proof

        let C1,C2 be strict discrete category;

        assume

         A15: the carrier of C1 = X & the carrier of C2 = X;

        

         A16: for C be discrete with_identities CategoryStr, x be object st C is non empty holds x in the composition of C iff ex f be morphism of C st x = [ [f, f], f]

        proof

          let C be discrete with_identities CategoryStr;

          let x be object;

          assume

           A17: C is non empty;

          hereby

            assume

             A18: x in the composition of C;

            then

            consider y,f be object such that

             A19: y in [:the carrier of C, the carrier of C:] & f in the carrier of C & x = [y, f] by ZFMISC_1:def 2;

            reconsider f as morphism of C by A19;

            take f;

            consider f1,f2 be object such that

             A20: f1 in the carrier of C & f2 in the carrier of C & y = [f1, f2] by A19, ZFMISC_1:def 2;

            reconsider f1, f2 as morphism of C by A20;

            

             A21: [f1, f2] in ( dom the composition of C) by A20, A19, A18, XTUPLE_0:def 12;

            

             A22: f1 |> f2 by A20, A19, A18, XTUPLE_0:def 12;

            then f1 = f2 & (f1 (*) f2) = f2 by Th21;

            then (the composition of C . (f1,f2)) = f2 by A21, Def3, Def2;

            then (the composition of C . y) = f2 by A20, BINOP_1:def 1;

            then f = f2 by A18, A19, FUNCT_1: 1;

            hence x = [ [f, f], f] by A22, A20, A19, Th21;

          end;

          given f be morphism of C such that

           A23: x = [ [f, f], f];

          consider f1 be morphism of C such that

           A24: f1 |> f & f1 is left_identity by A17, Def6, Def12;

          

           A25: f is identity by Def15;

          

           A26: f1 = (f1 (*) f) by A25, A24, Def5

          .= f by A24;

          f = (f (*) f) by A24, A26;

          then (the composition of C . (f,f)) = f by A24, A26, Def3;

          then (the composition of C . [f, f]) = f by BINOP_1:def 1;

          hence x in the composition of C by A23, A24, A26, FUNCT_1: 1;

        end;

        per cases ;

          suppose the carrier of C1 is empty;

          hence thesis by A15;

        end;

          suppose the carrier of C1 is non empty;

          then

           A27: C1 is non empty & C2 is non empty by A15;

          for x be object holds x in the composition of C1 iff x in the composition of C2

          proof

            let x be object;

            hereby

              assume x in the composition of C1;

              then

              consider f be morphism of C1 such that

               A28: x = [ [f, f], f] by A27, A16;

              reconsider f1 = f as morphism of C2 by A15;

              x = [ [f1, f1], f1] by A28;

              hence x in the composition of C2 by A27, A16;

            end;

            assume x in the composition of C2;

            then

            consider f be morphism of C2 such that

             A29: x = [ [f, f], f] by A27, A16;

            reconsider f1 = f as morphism of C1 by A15;

            x = [ [f1, f1], f1] by A29;

            hence x in the composition of C1 by A27, A16;

          end;

          hence thesis by A15, TARSKI: 2;

        end;

      end;

    end

    registration

      cluster strict for category;

      correctness

      proof

        set C = ( DiscreteCat the empty set);

        take C;

        thus thesis;

      end;

      cluster strict empty for category;

      correctness

      proof

        set C = ( DiscreteCat the empty set);

        take C;

        thus thesis by Def16;

      end;

      cluster strict non empty for category;

      correctness

      proof

        set C = ( DiscreteCat the non empty set);

        take C;

        thus thesis by Def16;

      end;

    end

    definition

      let C;

      :: CAT_6:def17

      func Ob (C) -> Subset of ( Mor C) equals { f where f be morphism of C : f is identity & f in ( Mor C) };

      correctness

      proof

        set O = { f where f be morphism of C : f is identity & f in ( Mor C) };

        for x be object st x in O holds x in ( Mor C)

        proof

          let x be object;

          assume x in O;

          then

          consider f be morphism of C such that

           A1: x = f & f is identity & f in ( Mor C);

          thus thesis by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let C;

      mode Object of C is Element of ( Ob C);

    end

    registration

      let C be non empty with_identities CategoryStr;

      cluster ( Ob C) -> non empty;

      correctness

      proof

        consider f be object such that

         A1: f in ( Mor C) by XBOOLE_0:def 1;

        reconsider f as morphism of C by A1;

        consider c be morphism of C such that

         A2: c |> f & c is left_identity by Def12, Def6;

        c is identity by A2, Th9;

        then c in { u where u be morphism of C : u is identity & u in ( Mor C) };

        hence thesis;

      end;

    end

    theorem :: CAT_6:22

    

     Th22: for C be non empty with_identities CategoryStr, f be morphism of C holds f is identity iff f is Object of C

    proof

      let C be non empty with_identities CategoryStr;

      let f be morphism of C;

      hereby

        assume f is identity;

        then f in { u where u be morphism of C : u is identity & u in ( Mor C) };

        hence f is Object of C;

      end;

      assume f is Object of C;

      then f in { u where u be morphism of C : u is identity & u in ( Mor C) };

      then

      consider u be morphism of C such that

       A1: f = u & u is identity & u in ( Mor C);

      thus f is identity by A1;

    end;

    theorem :: CAT_6:23

    

     Th23: for C be non empty with_identities CategoryStr, f,f1 be morphism of C, o be Object of C st f = o holds (f |> f1 implies (f (*) f1) = f1) & (f1 |> f implies (f1 (*) f) = f1) & f |> f

    proof

      let C be non empty with_identities CategoryStr;

      let f,f1 be morphism of C;

      let o be Object of C;

      assume

       A1: f = o;

      

       A2: f is identity by A1, Th22;

      consider c be morphism of C such that

       A3: c |> f & c is left_identity by Def12, Def6;

      

       A4: c = (c (*) f) by A2, A3, Def5

      .= f by A3;

      thus f |> f1 implies (f (*) f1) = f1 by A2, Def4;

      thus f1 |> f implies (f1 (*) f) = f1 by A2, Def5;

      thus f |> f by A3, A4;

    end;

    theorem :: CAT_6:24

    

     Th24: for C be non empty with_identities CategoryStr, f be morphism of C st f is identity holds f |> f

    proof

      let C be non empty with_identities CategoryStr;

      let f be morphism of C;

      assume f is identity;

      then f is Object of C by Th22;

      hence thesis by Th23;

    end;

    theorem :: CAT_6:25

    

     Th25: for C1,C2 be with_identities CategoryStr st the CategoryStr of C1 = the CategoryStr of C2 holds for f1 be morphism of C1, f2 be morphism of C2 st f1 = f2 holds f1 is identity iff f2 is identity

    proof

      let C1,C2 be with_identities CategoryStr;

      assume

       A1: the CategoryStr of C1 = the CategoryStr of C2;

      let f1 be morphism of C1;

      let f2 be morphism of C2;

      assume

       A2: f1 = f2;

      hereby

        assume

         A3: f1 is identity;

        

         A4: for f be morphism of C2 st f2 |> f holds (f2 (*) f) = f

        proof

          let f be morphism of C2;

          assume

           A5: f2 |> f;

          reconsider f3 = f as morphism of C1 by A1;

          

          thus (f2 (*) f) = (the composition of C2 . (f2,f)) by A5, Def3

          .= (f1 (*) f3) by A5, A2, A1, Def3, Def2

          .= f by A5, A3, Def4, Def2, A1, A2;

        end;

        for f be morphism of C2 st (f,f2) are_composable holds (f (*) f2) = f

        proof

          let f be morphism of C2;

          assume

           A6: f |> f2;

          reconsider f3 = f as morphism of C1 by A1;

          

          thus (f (*) f2) = (the composition of C2 . (f,f2)) by A6, Def3

          .= (f3 (*) f1) by A6, A2, A1, Def3, Def2

          .= f by A6, A3, Def5, Def2, A1, A2;

        end;

        then f2 is right_identity;

        hence f2 is identity by A4, Def4;

      end;

      assume

       A7: f2 is identity;

      

       A8: for f be morphism of C1 st f1 |> f holds (f1 (*) f) = f

      proof

        let f be morphism of C1;

        assume

         A9: f1 |> f;

        reconsider f3 = f as morphism of C2 by A1;

        

        thus (f1 (*) f) = (the composition of C1 . (f1,f)) by A9, Def3

        .= (f2 (*) f3) by A9, A2, A1, Def3, Def2

        .= f by A9, A7, Def4, Def2, A1, A2;

      end;

      for f be morphism of C1 st f |> f1 holds (f (*) f1) = f

      proof

        let f be morphism of C1;

        assume

         A10: f |> f1;

        reconsider f3 = f as morphism of C2 by A1;

        

        thus (f (*) f1) = (the composition of C1 . (f,f1)) by A10, Def3

        .= (f3 (*) f2) by A10, A2, A1, Def3, Def2

        .= f by A10, A7, Def5, Def2, A1, A2;

      end;

      then f1 is right_identity;

      hence f1 is identity by A8, Def4;

    end;

    

     Lm2: for C be CategoryStr holds C is with_identities iff for f be morphism of C st f in ( Mor C) holds (ex c be morphism of C st c |> f & c is identity) & (ex d be morphism of C st f |> d & d is identity)

    proof

      let C be CategoryStr;

      hereby

        assume

         A1: C is with_identities;

        let f be morphism of C;

        assume

         A2: f in ( Mor C);

        thus (ex c be morphism of C st c |> f & c is identity)

        proof

          consider c be morphism of C such that

           A3: c |> f & c is left_identity by A2, A1, Def6;

          take c;

          thus c |> f by A3;

          thus c is identity by A3, Th9, A1;

        end;

        consider d be morphism of C such that

         A4: f |> d & d is right_identity by A2, A1, Def7;

        take d;

        thus f |> d by A4;

        thus d is identity by A4, A1, Th9;

      end;

      assume

       A5: for f be morphism of C st f in ( Mor C) holds (ex c be morphism of C st c |> f & c is identity) & (ex d be morphism of C st f |> d & d is identity);

      for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f |> f1 & f is left_identity

      proof

        let f1 be morphism of C;

        assume f1 in the carrier of C;

        then

        consider f be morphism of C such that

         A6: f |> f1 & f is identity by A5;

        take f;

        thus f |> f1 by A6;

        thus f is left_identity by A6;

      end;

      then

       A7: C is with_left_identities;

      for f1 be morphism of C st f1 in the carrier of C holds ex f be morphism of C st f1 |> f & f is right_identity

      proof

        let f1 be morphism of C;

        assume f1 in the carrier of C;

        then

        consider f be morphism of C such that

         A8: f1 |> f & f is identity by A5;

        take f;

        thus f1 |> f by A8;

        thus f is right_identity by A8;

      end;

      hence C is with_identities by A7, Def7;

    end;

    

     Lm3: for C be CategoryStr holds C is composable iff for f,g,h be morphism of C holds ((h (*) g) |> f & h |> g implies g |> f) & (h |> (g (*) f) & g |> f implies h |> g) & (g |> f & h |> g implies (h (*) g) |> f & h |> (g (*) f))

    proof

      let C be CategoryStr;

      hereby

        assume C is composable;

        then

         A1: C is left_composable & C is right_composable;

        let f,g,h be morphism of C;

        thus (h (*) g) |> f & h |> g implies g |> f by A1;

        thus h |> (g (*) f) & g |> f implies h |> g by A1;

        assume

         A2: g |> f;

        assume

         A3: h |> g;

        thus (h (*) g) |> f by A2, A3, A1;

        thus h |> (g (*) f) by A2, A3, A1;

      end;

      assume

       A4: for f,g,h be morphism of C holds ((h (*) g) |> f & h |> g implies g |> f) & (h |> (g (*) f) & g |> f implies h |> g) & (g |> f & h |> g implies (h (*) g) |> f & h |> (g (*) f));

      then

       A5: C is left_composable;

      for f,f1,f2 be morphism of C st f1 |> f2 holds f |> (f1 (*) f2) iff f |> f1 by A4;

      hence C is composable by A5, Def9;

    end;

    definition

      let C be composable with_identities CategoryStr;

      let f be morphism of C;

      :: CAT_6:def18

      func dom f -> Object of C means

      : Def18: ex f1 be morphism of C st it = f1 & f |> f1 & f1 is identity if C is non empty

      otherwise it = the Object of C;

      existence

      proof

        thus not C is empty implies ex o be Object of C, f1 be morphism of C st o = f1 & f |> f1 & f1 is identity

        proof

          assume

           A1: not C is empty;

          then

          consider f1 be morphism of C such that

           A2: f |> f1 & f1 is identity by Lm2;

          reconsider o = f1 as Object of C by A2, A1, Th22;

          take o, f1;

          thus thesis by A2;

        end;

        assume C is empty;

        take the Object of C;

        thus thesis;

      end;

      uniqueness

      proof

        now

          let o1,o2 be Object of C;

          assume not C is empty;

          assume ex f1 be morphism of C st o1 = f1 & f |> f1 & f1 is identity;

          then

          consider f11 be morphism of C such that

           A3: o1 = f11 & f |> f11 & f11 is identity;

          assume ex f1 be morphism of C st o2 = f1 & f |> f1 & f1 is identity;

          then

          consider f12 be morphism of C such that

           A4: o2 = f12 & f |> f12 & f12 is identity;

          (f (*) f11) = f & (f (*) f12) = f by A3, A4, Def5;

          then

           A5: f11 |> f12 by A3, A4, Lm3;

          f11 = (f11 (*) f12) by A5, A4, Def5

          .= f12 by A5, A3, Def4;

          hence o1 = o2 by A3, A4;

        end;

        hence thesis;

      end;

      correctness ;

      :: CAT_6:def19

      func cod f -> Object of C means

      : Def19: ex f1 be morphism of C st it = f1 & f1 |> f & f1 is identity if C is non empty

      otherwise it = the Object of C;

      existence

      proof

        thus not C is empty implies ex o be Object of C, f1 be morphism of C st o = f1 & f1 |> f & f1 is identity

        proof

          assume

           A6: not C is empty;

          then

          consider f1 be morphism of C such that

           A7: f1 |> f & f1 is identity by Lm2;

          reconsider o = f1 as Object of C by A7, A6, Th22;

          take o, f1;

          thus thesis by A7;

        end;

        assume C is empty;

        take the Object of C;

        thus thesis;

      end;

      uniqueness

      proof

        now

          let o1,o2 be Object of C;

          assume not C is empty;

          assume ex f1 be morphism of C st o1 = f1 & f1 |> f & f1 is identity;

          then

          consider f11 be morphism of C such that

           A8: o1 = f11 & f11 |> f & f11 is identity;

          assume ex f1 be morphism of C st o2 = f1 & f1 |> f & f1 is identity;

          then

          consider f12 be morphism of C such that

           A9: o2 = f12 & f12 |> f & f12 is identity;

          (f11 (*) f) = f & (f12 (*) f) = f by A8, A9, Def4;

          then

           A10: f11 |> f12 by A8, A9, Lm3;

          f11 = (f11 (*) f12) by A10, A9, Def5

          .= f12 by A10, A8, Def4;

          hence o1 = o2 by A8, A9;

        end;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: CAT_6:26

    

     Th26: for C be composable with_identities CategoryStr, f,f1 be morphism of C st f |> f1 & f1 is identity holds ( dom f) = f1

    proof

      let C be composable with_identities CategoryStr;

      let f,f1 be morphism of C;

      assume

       A1: f |> f1 & f1 is identity;

      then

       A2: C is non empty;

      then

      reconsider o = f1 as Object of C by A1, Th22;

      ex f11 be morphism of C st o = f11 & f |> f11 & f11 is identity by A1;

      hence ( dom f) = f1 by A2, Def18;

    end;

    theorem :: CAT_6:27

    

     Th27: for C be composable with_identities CategoryStr, f,f1 be morphism of C st f1 |> f & f1 is identity holds ( cod f) = f1

    proof

      let C be composable with_identities CategoryStr;

      let f,f1 be morphism of C;

      assume

       A1: f1 |> f & f1 is identity;

      then

       A2: C is non empty;

      then

      reconsider o = f1 as Object of C by A1, Th22;

      ex f11 be morphism of C st o = f11 & f11 |> f & f11 is identity by A1;

      hence ( cod f) = f1 by A2, Def19;

    end;

    definition

      let C be with_identities CategoryStr;

      let o be Object of C;

      :: CAT_6:def20

      func id- o -> morphism of C equals o;

      correctness

      proof

        per cases ;

          suppose C is empty;

          hence thesis;

        end;

          suppose not C is empty;

          then not ( Ob C) is empty;

          then o in ( Ob C);

          hence thesis;

        end;

      end;

    end

    definition

      let C,D be CategoryStr;

      mode Functor of C,D is Function of C, D;

    end

    reserve C,D,E for with_identities CategoryStr;

    reserve F for Functor of C, D;

    reserve G for Functor of D, E;

    reserve f for morphism of C;

    definition

      let C, D, F, f;

      :: CAT_6:def21

      func F . f -> morphism of D equals

      : Def21: (F . f) if C is non empty

      otherwise the Object of D;

      correctness

      proof

        thus not C is empty implies (F . f) is morphism of D

        proof

          assume

           A1: C is non empty;

          per cases ;

            suppose ( Mor D) <> {} ;

            hence thesis by A1, FUNCT_2: 5;

          end;

            suppose ( Mor D) = {} ;

            hence thesis by SUBSET_1:def 1;

          end;

        end;

         the Object of D is morphism of D

        proof

          per cases ;

            suppose ( Mor D) <> {} ;

            then D is non empty;

            hence thesis by TARSKI:def 3;

          end;

            suppose ( Mor D) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let C, D, F;

      :: CAT_6:def22

      attr F is identity-preserving means

      : Def22: for f be morphism of C st f is identity holds (F . f) is identity;

      :: CAT_6:def23

      attr F is multiplicative means

      : Def23: for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2));

      :: CAT_6:def24

      attr F is antimultiplicative means for f1,f2 be morphism of C st f1 |> f2 holds (F . f2) |> (F . f1) & (F . (f1 (*) f2)) = ((F . f2) (*) (F . f1));

    end

    registration

      let C, D;

      cluster identity-preserving for Functor of C, D;

      correctness

      proof

        per cases ;

          suppose ( Mor D) is non empty;

          then

          reconsider D1 = D as non empty with_identities CategoryStr;

          

           A1: ( Ob D1) is non empty;

          set F = (( Mor C) --> the Object of D);

           the Object of D in ( Ob D) by A1;

          then

          reconsider F as Function of C, D by FUNCOP_1: 45;

          take F;

          for f be morphism of C st f is identity holds (F . f) is identity

          proof

            let f be morphism of C;

            assume f is identity;

            reconsider x = f as object;

            per cases ;

              suppose

               A2: C is non empty;

              (F . f) = (F . x) by A2, Def21

              .= the Object of D by A2, FUNCOP_1: 7;

              then (F . f) is Object of D1;

              hence (F . f) is identity by Th22;

            end;

              suppose C is empty;

              then (F . f) is Object of D1 by Def21;

              hence thesis by Th22;

            end;

          end;

          hence thesis;

        end;

          suppose

           A3: ( Mor D) is empty;

          set F = the Function of C, D;

          take F;

          for f be morphism of C st f is identity holds (F . f) is identity

          proof

            let f be morphism of C;

            assume f is identity;

            D is empty by A3;

            hence (F . f) is identity by Th10;

          end;

          hence thesis;

        end;

      end;

    end

    registration

      let C be empty with_identities CategoryStr;

      let D be with_identities CategoryStr;

      cluster identity-preserving multiplicative antimultiplicative for Functor of C, D;

      correctness

      proof

        per cases ;

          suppose ( Mor D) is non empty;

          then

          reconsider D1 = D as non empty with_identities CategoryStr;

          set F = (( Mor C) --> the Object of D);

          reconsider F as Function of C, D;

          take F;

          

           A1: for f be morphism of C st f is identity holds (F . f) is identity

          proof

            let f be morphism of C;

            assume f is identity;

            (F . f) is Object of D1 by Def21;

            hence thesis by Th22;

          end;

          (for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2))) & (for f1,f2 be morphism of C st f1 |> f2 holds (F . f2) |> (F . f1) & (F . (f1 (*) f2)) = ((F . f2) (*) (F . f1)));

          hence thesis by A1;

        end;

          suppose

           A2: ( Mor D) is empty;

          set F = the Function of C, D;

          take F;

          

           A3: for f be morphism of C st f is identity holds (F . f) is identity

          proof

            let f be morphism of C;

            assume f is identity;

            D is empty by A2;

            hence (F . f) is identity by Th10;

          end;

          (for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2))) & (for f1,f2 be morphism of C st f1 |> f2 holds (F . f2) |> (F . f1) & (F . (f1 (*) f2)) = ((F . f2) (*) (F . f1)));

          hence thesis by A3;

        end;

      end;

    end

    registration

      let C be with_identities CategoryStr;

      let D be non empty with_identities CategoryStr;

      cluster identity-preserving multiplicative antimultiplicative for Functor of C, D;

      correctness

      proof

        per cases ;

          suppose

           A1: C is non empty;

          set F = (( Mor C) --> the Object of D);

           the Object of D in ( Ob D);

          then

          reconsider F as Function of C, D by FUNCOP_1: 45;

          take F;

          

           A2: for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2))

          proof

            let f1,f2 be morphism of C;

            assume f1 |> f2;

            reconsider x1 = f1, x2 = f2, x3 = (f1 (*) f2) as object;

            

             A3: (F . f1) = (F . x1) by A1, Def21

            .= the Object of D by A1, FUNCOP_1: 7;

            

             A4: (F . f2) = (F . x2) by A1, Def21

            .= the Object of D by A1, FUNCOP_1: 7;

            

             A5: (F . (f1 (*) f2)) = (F . x3) by A1, Def21

            .= the Object of D by A1, FUNCOP_1: 7;

            thus

             A6: (F . f1) |> (F . f2) by A3, A4, Th23;

            thus (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2)) by A4, A5, A3, A6, Th23;

          end;

          

           A7: for f1,f2 be morphism of C st f1 |> f2 holds (F . f2) |> (F . f1) & (F . (f1 (*) f2)) = ((F . f2) (*) (F . f1))

          proof

            let f1,f2 be morphism of C;

            assume f1 |> f2;

            reconsider x1 = f1, x2 = f2, x3 = (f1 (*) f2) as object;

            

             A8: (F . f1) = (F . x1) by A1, Def21

            .= the Object of D by A1, FUNCOP_1: 7;

            

             A9: (F . f2) = (F . x2) by A1, Def21

            .= the Object of D by A1, FUNCOP_1: 7;

            

             A10: (F . (f1 (*) f2)) = (F . x3) by A1, Def21

            .= the Object of D by A1, FUNCOP_1: 7;

            thus

             A11: (F . f2) |> (F . f1) by A8, A9, Th23;

            thus (F . (f1 (*) f2)) = ((F . f2) (*) (F . f1)) by A9, A10, A8, A11, Th23;

          end;

          for f be morphism of C st f is identity holds (F . f) is identity

          proof

            let f be morphism of C;

            assume f is identity;

            reconsider x = f as object;

            (F . f) = (F . x) by A1, Def21

            .= the Object of D by A1, FUNCOP_1: 7;

            hence (F . f) is identity by Th22;

          end;

          hence thesis by A2, A7;

        end;

          suppose

           A12: C is empty;

          set F = the Function of C, D;

          take F;

          

           A13: for f be morphism of C st f is identity holds (F . f) is identity

          proof

            let f be morphism of C;

            assume f is identity;

            (F . f) = the Object of D by A12, Def21;

            hence (F . f) is identity by Th22;

          end;

          (for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2))) & (for f1,f2 be morphism of C st f1 |> f2 holds (F . f2) |> (F . f1) & (F . (f1 (*) f2)) = ((F . f2) (*) (F . f1))) by A12;

          hence thesis by A13;

        end;

      end;

    end

    theorem :: CAT_6:28

    ex C,D be category, F be Functor of C, D st F is multiplicative & F is non identity-preserving

    proof

      set C = the non empty category;

      reconsider X = { 0 , 1} as set;

      set comp = ( { [ [ 0 , 0 ], 0 ], [ [1, 1], 1]} \/ { [ [ 0 , 1], 1], [ [1, 0 ], 1]});

      

       A1: for x be object holds x in comp iff (x = [ [ 0 , 0 ], 0 ] or x = [ [1, 1], 1] or x = [ [ 0 , 1], 1] or x = [ [1, 0 ], 1])

      proof

        let x be object;

        thus x in comp implies (x = [ [ 0 , 0 ], 0 ] or x = [ [1, 1], 1] or x = [ [ 0 , 1], 1] or x = [ [1, 0 ], 1])

        proof

          assume x in comp;

          then x in { [ [ 0 , 0 ], 0 ], [ [1, 1], 1]} or x in { [ [ 0 , 1], 1], [ [1, 0 ], 1]} by XBOOLE_0:def 3;

          hence thesis by TARSKI:def 2;

        end;

        assume x = [ [ 0 , 0 ], 0 ] or x = [ [1, 1], 1] or x = [ [ 0 , 1], 1] or x = [ [1, 0 ], 1];

        then x in { [ [ 0 , 0 ], 0 ], [ [1, 1], 1]} or x in { [ [ 0 , 1], 1], [ [1, 0 ], 1]} by TARSKI:def 2;

        hence x in comp by XBOOLE_0:def 3;

      end;

      

       A2: for x,y1,y2 be object st [x, y1] in comp & [x, y2] in comp holds y1 = y2

      proof

        let x,y1,y2 be object;

        assume

         A3: [x, y1] in comp;

        assume

         A4: [x, y2] in comp;

        per cases by A3, A1;

          suppose

           A5: [x, y1] = [ [ 0 , 0 ], 0 ];

          then

           A6: x = [ 0 , 0 ] & y1 = 0 by XTUPLE_0: 1;

          per cases by A4, A1;

            suppose [x, y2] = [ [ 0 , 0 ], 0 ];

            hence thesis by A5, XTUPLE_0: 1;

          end;

            suppose [x, y2] = [ [1, 1], 1];

            then x = [1, 1] & y2 = 1 by XTUPLE_0: 1;

            hence thesis by A6, XTUPLE_0: 1;

          end;

            suppose [x, y2] = [ [ 0 , 1], 1];

            then x = [ 0 , 1] & y2 = 1 by XTUPLE_0: 1;

            hence thesis by A6, XTUPLE_0: 1;

          end;

            suppose [x, y2] = [ [1, 0 ], 1];

            then x = [1, 0 ] & y2 = 1 by XTUPLE_0: 1;

            hence thesis by A6, XTUPLE_0: 1;

          end;

        end;

          suppose [x, y1] = [ [1, 1], 1];

          then

           A7: x = [1, 1] & y1 = 1 by XTUPLE_0: 1;

          per cases by A4, A1;

            suppose [x, y2] = [ [ 0 , 0 ], 0 ];

            then x = [ 0 , 0 ] & y2 = 0 by XTUPLE_0: 1;

            hence thesis by A7, XTUPLE_0: 1;

          end;

            suppose [x, y2] = [ [1, 1], 1] or [x, y2] = [ [ 0 , 1], 1] or [x, y2] = [ [1, 0 ], 1];

            hence thesis by A7, XTUPLE_0: 1;

          end;

        end;

          suppose [x, y1] = [ [ 0 , 1], 1];

          then

           A8: x = [ 0 , 1] & y1 = 1 by XTUPLE_0: 1;

          per cases by A4, A1;

            suppose [x, y2] = [ [ 0 , 0 ], 0 ];

            then x = [ 0 , 0 ] & y2 = 0 by XTUPLE_0: 1;

            hence thesis by A8, XTUPLE_0: 1;

          end;

            suppose [x, y2] = [ [1, 1], 1] or [x, y2] = [ [ 0 , 1], 1] or [x, y2] = [ [1, 0 ], 1];

            hence thesis by A8, XTUPLE_0: 1;

          end;

        end;

          suppose [x, y1] = [ [1, 0 ], 1];

          then

           A9: x = [1, 0 ] & y1 = 1 by XTUPLE_0: 1;

          per cases by A4, A1;

            suppose [x, y2] = [ [ 0 , 0 ], 0 ];

            then x = [ 0 , 0 ] & y2 = 0 by XTUPLE_0: 1;

            hence thesis by A9, XTUPLE_0: 1;

          end;

            suppose [x, y2] = [ [1, 1], 1] or [x, y2] = [ [ 0 , 1], 1] or [x, y2] = [ [1, 0 ], 1];

            hence thesis by A9, XTUPLE_0: 1;

          end;

        end;

      end;

      for x be object st x in comp holds x in [: [:X, X:], X:]

      proof

        let x be object;

        assume

         A10: x in comp;

        per cases by A10, A1;

          suppose

           A11: x = [ [ 0 , 0 ], 0 ];

          

           A12: 0 in X by TARSKI:def 2;

          then [ 0 , 0 ] in [:X, X:] by ZFMISC_1:def 2;

          hence x in [: [:X, X:], X:] by A11, A12, ZFMISC_1:def 2;

        end;

          suppose

           A13: x = [ [1, 1], 1];

          

           A14: 1 in X by TARSKI:def 2;

          then [1, 1] in [:X, X:] by ZFMISC_1:def 2;

          hence x in [: [:X, X:], X:] by A13, A14, ZFMISC_1:def 2;

        end;

          suppose

           A15: x = [ [ 0 , 1], 1];

          

           A16: 0 in X & 1 in X by TARSKI:def 2;

          then [ 0 , 1] in [:X, X:] by ZFMISC_1:def 2;

          hence x in [: [:X, X:], X:] by A15, A16, ZFMISC_1:def 2;

        end;

          suppose

           A17: x = [ [1, 0 ], 1];

          

           A18: 0 in X & 1 in X by TARSKI:def 2;

          then [1, 0 ] in [:X, X:] by ZFMISC_1:def 2;

          hence x in [: [:X, X:], X:] by A17, A18, ZFMISC_1:def 2;

        end;

      end;

      then

      reconsider comp as PartFunc of [:X, X:], X by A2, TARSKI:def 3, FUNCT_1:def 1;

      set D = CategoryStr (# X, comp #);

      

       A19: for f1,f2 be morphism of D st f1 |> f2 holds (f1 = 0 & f2 = 0 & (f1 (*) f2) = 0 ) or (f1 = 1 & f2 = 1 & (f1 (*) f2) = 1) or (f1 = 0 & f2 = 1 & (f1 (*) f2) = 1) or (f1 = 1 & f2 = 0 & (f1 (*) f2) = 1)

      proof

        let f1,f2 be morphism of D;

        assume

         A20: f1 |> f2;

        assume

         A21: not (f1 = 0 & f2 = 0 & (f1 (*) f2) = 0 ) & not (f1 = 1 & f2 = 1 & (f1 (*) f2) = 1) & not (f1 = 0 & f2 = 1 & (f1 (*) f2) = 1);

        consider y be object such that

         A22: [ [f1, f2], y] in the composition of D by A20, XTUPLE_0:def 12;

        

         A23: (f1 (*) f2) = (the composition of D . (f1,f2)) by Def3, A20

        .= (the composition of D . [f1, f2]) by BINOP_1:def 1

        .= y by A22, FUNCT_1: 1;

        per cases by A22, A1;

          suppose [ [f1, f2], y] = [ [ 0 , 0 ], 0 ];

          then [f1, f2] = [ 0 , 0 ] & y = 0 by XTUPLE_0: 1;

          hence thesis by A23, A21, XTUPLE_0: 1;

        end;

          suppose [ [f1, f2], y] = [ [1, 1], 1];

          then [f1, f2] = [1, 1] & y = 1 by XTUPLE_0: 1;

          hence thesis by A21, A23, XTUPLE_0: 1;

        end;

          suppose [ [f1, f2], y] = [ [ 0 , 1], 1];

          then [f1, f2] = [ 0 , 1] & y = 1 by XTUPLE_0: 1;

          hence thesis by A21, A23, XTUPLE_0: 1;

        end;

          suppose [ [f1, f2], y] = [ [1, 0 ], 1];

          then [f1, f2] = [1, 0 ] & y = 1 by XTUPLE_0: 1;

          hence thesis by A23, XTUPLE_0: 1;

        end;

      end;

      

       A24: for f1,f2 be morphism of D holds f1 |> f2

      proof

        let f1,f2 be morphism of D;

        per cases by TARSKI:def 2;

          suppose (f1 = 0 & f2 = 0 ) or (f1 = 1 & f2 = 1) or (f1 = 0 & f2 = 1);

          then [ [f1, f2], f2] in the composition of D by A1;

          hence thesis by FUNCT_1: 1;

        end;

          suppose f1 = 1 & f2 = 0 ;

          then [ [f1, f2], f1] in the composition of D by A1;

          hence thesis by FUNCT_1: 1;

        end;

      end;

      

       A25: D is left_composable by A24;

      

       A26: for f,f1,f2 be morphism of D st f1 |> f2 holds f |> (f1 (*) f2) iff f |> f1 by A24;

      

       A27: for f1 be morphism of D st f1 in the carrier of D holds ex f be morphism of D st f |> f1 & f is left_identity

      proof

        let f1 be morphism of D;

        assume f1 in the carrier of D;

        reconsider f = 0 as morphism of D by TARSKI:def 2;

        take f;

        thus f |> f1 by A24;

        for f2 be morphism of D st f |> f2 holds (f (*) f2) = f2

        proof

          let f2 be morphism of D;

          assume

           A28: f |> f2;

          f2 = 0 or f2 = 1 by TARSKI:def 2;

          hence (f (*) f2) = f2 by A28, A19;

        end;

        hence f is left_identity;

      end;

      for f1 be morphism of D st f1 in the carrier of D holds ex f be morphism of D st f1 |> f & f is right_identity

      proof

        let f1 be morphism of D;

        assume f1 in the carrier of D;

        reconsider f = 0 as morphism of D by TARSKI:def 2;

        take f;

        thus f1 |> f by A24;

        for f2 be morphism of D st f2 |> f holds (f2 (*) f) = f2

        proof

          let f2 be morphism of D;

          assume

           A29: f2 |> f;

          f2 = 0 or f2 = 1 by TARSKI:def 2;

          hence (f2 (*) f) = f2 by A29, A19;

        end;

        hence f is right_identity;

      end;

      then

       A30: D is with_right_identities;

      for f1,f2,f3 be morphism of D st f1 |> f2 & f2 |> f3 & (f1 (*) f2) |> f3 & f1 |> (f2 (*) f3) holds (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3)

      proof

        let f1,f2,f3 be morphism of D;

        assume

         A31: f1 |> f2 & f2 |> f3;

        assume

         A32: (f1 (*) f2) |> f3;

        assume

         A33: f1 |> (f2 (*) f3);

        per cases by TARSKI:def 2;

          suppose

           A34: f3 = 0 ;

          per cases by TARSKI:def 2;

            suppose

             A35: f2 = 0 ;

            then

             A36: (f2 (*) f3) = 0 by A34, A31, A19;

            per cases by TARSKI:def 2;

              suppose f1 = 0 ;

              hence (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3) by A36, A34, A35;

            end;

              suppose

               A37: f1 = 1;

              then

               A38: (f1 (*) f2) = 1 by A31, A19;

              

              thus (f1 (*) (f2 (*) f3)) = 1 by A37, A33, A19

              .= ((f1 (*) f2) (*) f3) by A32, A38, A19;

            end;

          end;

            suppose

             A39: f2 = 1;

            then (f2 (*) f3) = 1 & (f1 (*) f2) = 1 by A31, A19;

            hence (f1 (*) (f2 (*) f3)) = ((f1 (*) f2) (*) f3) by A39;

          end;

        end;

          suppose

           A40: f3 = 1;

          then (f2 (*) f3) = 1 by A31, A19;

          

          hence (f1 (*) (f2 (*) f3)) = 1 by A33, A19

          .= ((f1 (*) f2) (*) f3) by A32, A40, A19;

        end;

      end;

      then

      reconsider D as category by A26, A27, A30, Def6, Def10, Def12, A25, Def9, Def11;

      take C, D;

      reconsider d1 = 1 as morphism of D by TARSKI:def 2;

      deffunc F1( object) = d1;

      

       A41: for x be object st x in the carrier of C holds F1(x) in the carrier of D;

      consider F be Function of the carrier of C, the carrier of D such that

       A42: for x be object st x in the carrier of C holds (F . x) = F1(x) from FUNCT_2:sch 2( A41);

      reconsider F as Functor of C, D;

      take F;

      for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2))

      proof

        let f1,f2 be morphism of C;

        assume f1 |> f2;

        thus (F . f1) |> (F . f2) by A24;

        reconsider x1 = f1, x2 = f2, x12 = (f1 (*) f2) as object;

        

         A43: (F . f1) = (F . x1) by Def21

        .= d1 by A42;

        

         A44: (F . f2) = (F . x2) by Def21

        .= d1 by A42;

        

         A45: d1 |> d1 by A24;

        

        thus (F . (f1 (*) f2)) = (F . x12) by Def21

        .= d1 by A42

        .= ((F . f1) (*) (F . f2)) by A43, A44, A45, A19;

      end;

      hence F is multiplicative;

      ex f be morphism of C st f is identity & not (F . f) is identity

      proof

        reconsider f = the Object of C as morphism of C by TARSKI:def 3;

        take f;

        thus f is identity by Th22;

        reconsider x = f as object;

        

         A46: (F . f) = (F . x) by Def21

        .= d1 by A42;

        ex d0 be morphism of D st d1 |> d0 & not (d1 (*) d0) = d0

        proof

          reconsider d0 = 0 as morphism of D by TARSKI:def 2;

          take d0;

          thus d1 |> d0 by A24;

          hence not (d1 (*) d0) = d0 by A19;

        end;

        hence not (F . f) is identity by A46, Def4;

      end;

      hence F is non identity-preserving;

    end;

    theorem :: CAT_6:29

    

     Th29: C is non empty & D is empty implies not ex F be Functor of C, D st F is multiplicative or F is antimultiplicative

    proof

      assume

       A1: C is non empty;

      then

      reconsider f = the Object of C as morphism of C by TARSKI:def 3;

      

       A2: f |> f by A1, Th23;

      assume

       A3: D is empty;

      assume ex F be Functor of C, D st F is multiplicative or F is antimultiplicative;

      then

      consider F be Functor of C, D such that

       A4: F is multiplicative or F is antimultiplicative;

      

       A5: not (F . f) |> (F . f) by A3;

      per cases by A4;

        suppose F is multiplicative;

        hence thesis by A5, A2;

      end;

        suppose F is antimultiplicative;

        hence thesis by A5, A2;

      end;

    end;

    theorem :: CAT_6:30

    ex C,D be category, F be Functor of C, D st F is non multiplicative & F is identity-preserving

    proof

      set C = the non empty category;

      set D = the empty category;

      set F = the identity-preserving Functor of C, D;

      take C, D, F;

      thus thesis by Th29;

    end;

    definition

      let C, D, F;

      :: CAT_6:def25

      attr F is covariant means

      : Def25: F is identity-preserving & F is multiplicative;

      :: CAT_6:def26

      attr F is contravariant means F is identity-preserving & F is antimultiplicative;

    end

    registration

      let C be empty with_identities CategoryStr;

      let D be with_identities CategoryStr;

      cluster covariant contravariant for Functor of C, D;

      correctness

      proof

        set F = the identity-preserving multiplicative antimultiplicative Functor of C, D;

        take F;

        thus thesis;

      end;

    end

    registration

      let C be with_identities CategoryStr;

      let D be non empty with_identities CategoryStr;

      cluster covariant contravariant for Functor of C, D;

      correctness

      proof

        set F = the identity-preserving multiplicative antimultiplicative Functor of C, D;

        take F;

        thus thesis;

      end;

    end

    theorem :: CAT_6:31

    C is non empty & D is empty implies not ex F be Functor of C, D st F is covariant or F is contravariant by Th29;

    definition

      let C,D be non empty with_identities CategoryStr;

      let F be covariant Functor of C, D;

      let f be Object of C;

      :: original: .

      redefine

      func F . f -> Object of D ;

      coherence

      proof

        f in ( Ob C);

        then

        consider f1 be morphism of C such that

         A1: f = f1 & f1 is identity & f1 in ( Mor C);

        (F . f1) is identity & (F . f1) in ( Mor D) by A1, Def22, Def25;

        then (F . f1) in ( Ob D);

        hence thesis by A1, Def21;

      end;

    end

    theorem :: CAT_6:32

    

     Th32: for C,D be non empty composable with_identities CategoryStr, F be covariant Functor of C, D, f be morphism of C holds (F . ( dom f)) = ( dom (F . f)) & (F . ( cod f)) = ( cod (F . f))

    proof

      let C,D be non empty composable with_identities CategoryStr;

      let F be covariant Functor of C, D;

      let f be morphism of C;

      

       A1: F is multiplicative by Def25;

      consider d be morphism of C such that

       A2: ( dom f) = d & f |> d & d is identity by Def18;

      (F . ( dom f)) in ( Ob D);

      then

      reconsider d1 = (F . ( dom f)) as morphism of D;

      

       A3: (F . f) |> (F . d) by A2, A1;

      

       A4: (F . d) = (F . ( dom f)) by A2, Def21;

      d1 is identity by Th22;

      hence (F . ( dom f)) = ( dom (F . f)) by A3, A4, Def18;

      consider c be morphism of C such that

       A5: ( cod f) = c & c |> f & c is identity by Def19;

      (F . ( cod f)) in ( Ob D);

      then

      reconsider c1 = (F . ( cod f)) as morphism of D;

      

       A6: (F . c) |> (F . f) by A5, A1;

      

       A7: (F . c) = (F . ( cod f)) by A5, Def21;

      c1 is identity by Th22;

      hence (F . ( cod f)) = ( cod (F . f)) by A6, A7, Def19;

    end;

    theorem :: CAT_6:33

    for C,D be non empty composable with_identities CategoryStr, F be covariant Functor of C, D, o be Object of C holds (F . ( id- o)) = ( id- (F . o)) by Def21;

    definition

      let C, D, E;

      let F, G;

      assume

       A1: (F is covariant or F is contravariant) & (G is covariant or G is contravariant);

      :: CAT_6:def27

      func G (*) F -> Functor of C, E equals

      : Def27: (F * G);

      coherence

      proof

        set FG = (F * G);

        reconsider FG as PartFunc of the carrier of C, the carrier of E;

         not (C is non empty & D is empty) & not (D is non empty & E is empty) by A1, Th29;

        hence thesis;

      end;

    end

    theorem :: CAT_6:34

    

     Th34: F is covariant & G is covariant & C is non empty implies ((G (*) F) . f) = (G . (F . f))

    proof

      assume

       A1: F is covariant;

      assume

       A2: G is covariant;

      assume

       A3: C is non empty;

      then

       A4: D is non empty by A1, Th29;

      then

       A5: E is non empty by A2, Th29;

      reconsider x = f as object;

      

       A6: ( dom (G (*) F)) = the carrier of C by A5, FUNCT_2:def 1;

      

       A7: (F . x) = (F . f) by A3, Def21;

      then

       A8: (G . (F . x)) = (G . (F . f)) by A4, Def21;

      

       A9: ( dom F) = the carrier of C by A4, FUNCT_2:def 1;

      ( dom G) = the carrier of D by A5, FUNCT_2:def 1;

      then [x, (F . x)] in F & [(F . x), (G . (F . x))] in G by A3, A4, A9, A7, FUNCT_1: 1;

      then [f, (G . (F . f))] in (F * G) by A8, RELAT_1:def 8;

      then

       A10: [f, (G . (F . f))] in (G (*) F) by A1, A2, Def27;

      

      thus ((G (*) F) . f) = ((G (*) F) . x) by A3, Def21

      .= (G . (F . f)) by A10, A6, FUNCT_1:def 2;

    end;

    theorem :: CAT_6:35

    F is covariant & G is covariant implies (G (*) F) is covariant

    proof

      assume

       A1: F is covariant;

      assume

       A2: G is covariant;

      set GF = (G (*) F);

      for f be morphism of C st f is identity holds (GF . f) is identity

      proof

        let f be morphism of C;

        assume

         A3: f is identity;

        per cases ;

          suppose

           A4: C is non empty;

          

           A7: (F . f) is identity by A1, A3, Def22;

          ((G (*) F) . f) = (G . (F . f)) by A1, A2, Th34, A4;

          hence (GF . f) is identity by A2, A7, Def22;

        end;

          suppose

           A8: C is empty;

          per cases ;

            suppose

             A9: E is non empty;

            (GF . f) = the Object of E by A8, Def21;

            hence (GF . f) is identity by A9, Th22;

          end;

            suppose E is empty;

            hence (GF . f) is identity by Th10;

          end;

        end;

      end;

      then

       A10: GF is identity-preserving;

      for f1,f2 be morphism of C st f1 |> f2 holds (GF . f1) |> (GF . f2) & (GF . (f1 (*) f2)) = ((GF . f1) (*) (GF . f2))

      proof

        let f1,f2 be morphism of C;

        assume

         A11: f1 |> f2;

        then

         A12: C is non empty;

        

         A15: (GF . f1) = (G . (F . f1)) by A12, A1, A2, Th34;

        

         A16: G is multiplicative by A2;

        F is multiplicative by A1;

        then

         A17: (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2)) by A11;

        then (G . (F . f1)) |> (G . (F . f2)) & (G . ((F . f1) (*) (F . f2))) = ((G . (F . f1)) (*) (G . (F . f2))) by A16;

        hence (GF . f1) |> (GF . f2) by A15, A12, A1, A2, Th34;

        

        thus (GF . (f1 (*) f2)) = (G . (F . (f1 (*) f2))) by A12, A1, A2, Th34

        .= ((G . (F . f1)) (*) (G . (F . f2))) by A17, A16

        .= ((GF . f1) (*) (GF . f2)) by A15, A12, A1, A2, Th34;

      end;

      hence (G (*) F) is covariant by A10, Def23;

    end;

    definition

      let C;

      :: original: id

      redefine

      func id C -> Functor of C, C ;

      coherence ;

    end

    registration

      let C;

      cluster ( id C) -> covariant;

      correctness

      proof

        set F = ( id C);

        

         A1: F = ( id the carrier of C) by STRUCT_0:def 4;

        for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2))

        proof

          let f1,f2 be morphism of C;

          assume

           A2: f1 |> f2;

          per cases ;

            suppose

             A3: C is non empty;

            reconsider x1 = f1, x2 = f2, x3 = (f1 (*) f2) as object;

            

             A4: (F . f1) = (F . x1) by A3, Def21

            .= f1 by A1;

            

             A5: (F . f2) = (F . x2) by A3, Def21

            .= f2 by A1;

            

             A6: (F . (f1 (*) f2)) = (F . x3) by A3, Def21

            .= (f1 (*) f2) by A1;

            thus (F . f1) |> (F . f2) by A4, A5, A2;

            thus (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2)) by A4, A6, A5;

          end;

            suppose C is empty;

            hence thesis by A2;

          end;

        end;

        then

         A7: F is multiplicative;

        for f be morphism of C st f is identity holds (F . f) is identity

        proof

          let f be morphism of C;

          assume

           A8: f is identity;

          per cases ;

            suppose

             A9: C is non empty;

            reconsider x = f as object;

            (F . f) = (F . x) by A9, Def21

            .= f by A1;

            hence (F . f) is identity by A8;

          end;

            suppose C is empty;

            hence (F . f) is identity by Th10;

          end;

        end;

        hence thesis by A7, Def22;

      end;

    end

    definition

      let C, D;

      :: CAT_6:def28

      pred C,D are_isomorphic means ex F be Functor of C, D, G be Functor of D, C st F is covariant & G is covariant & (G (*) F) = ( id C) & (F (*) G) = ( id D);

      reflexivity

      proof

        let C be with_identities CategoryStr;

        set F = ( id C), G = ( id C);

        

         A1: F = ( id the carrier of C) & G = ( id the carrier of C) by STRUCT_0:def 4;

        take F, G;

        (G (*) F) = (( id the carrier of C) * ( id the carrier of C)) by A1, Def27

        .= ( id (the carrier of C /\ the carrier of C)) by FUNCT_1: 22

        .= ( id C) by STRUCT_0:def 4;

        hence thesis;

      end;

      symmetry ;

    end

    notation

      let C, D;

      synonym C ~= D for C,D are_isomorphic ;

    end

    begin

    

     Lm4: for C be CategoryStr, f,g be morphism of C st g |> f holds (g (*) f) = (the composition of C . [g, f])

    proof

      let C be CategoryStr;

      let f,g be morphism of C;

      assume g |> f;

      

      hence (g (*) f) = (the composition of C . (g,f)) by Def3

      .= (the composition of C . [g, f]) by BINOP_1:def 1;

    end;

    

     Lm5: for C be composable CategoryStr holds C is associative iff for f,g,h be morphism of C st h |> g & g |> f holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

    proof

      let C be composable CategoryStr;

      hereby

        assume

         A1: C is associative;

        

         A2: C is left_composable & C is right_composable by Def11;

        let f,g,h be morphism of C;

        assume

         A3: h |> g & g |> f;

        then (h (*) g) |> f & h |> (g (*) f) by A2;

        hence (h (*) (g (*) f)) = ((h (*) g) (*) f) by A3, A1;

      end;

      assume for f,g,h be morphism of C st h |> g & g |> f holds (h (*) (g (*) f)) = ((h (*) g) (*) f);

      hence C is associative;

    end;

    definition

      let C be CategoryStr;

      :: CAT_6:def29

      func CompMap (C) -> PartFunc of [:( Mor C), ( Mor C):], ( Mor C) equals the composition of C;

      correctness ;

    end

    definition

      let C be composable with_identities CategoryStr;

      :: CAT_6:def30

      func SourceMap (C) -> Function of ( Mor C), ( Ob C) means

      : Def30: for f be Element of ( Mor C) holds (it . f) = ( dom f) if C is non empty

      otherwise it = {} ;

      correctness

      proof

        

         A1: not C is empty implies ex F be Function of ( Mor C), ( Ob C) st for f be Element of ( Mor C) holds (F . f) = ( dom f)

        proof

          assume not C is empty;

          then

          reconsider A = ( Mor C), O = ( Ob C) as non empty set;

          defpred P[ set, set] means ex a be Element of ( Mor C), o be Element of ( Ob C) st a = $1 & o = $2 & o = ( dom a);

          

           A2: for x be Element of A holds ex y be Element of O st P[x, y]

          proof

            let x be Element of A;

            reconsider f = x as Element of ( Mor C);

            reconsider y = ( dom f) as Element of O;

            take y;

            thus P[x, y];

          end;

          consider F be Function of A, O such that

           A3: for x be Element of A holds P[x, (F . x)] from FUNCT_2:sch 3( A2);

          reconsider F as Function of ( Mor C), ( Ob C);

          take F;

          let f be Element of ( Mor C);

           P[f, (F . f)] by A3;

          hence thesis;

        end;

        

         A4: C is empty implies ex F be Function of ( Mor C), ( Ob C) st F = {}

        proof

          assume C is empty;

          then ( Mor C) = {} & ( Ob C) = {} ;

          then

          reconsider F = {} as Function of ( Mor C), ( Ob C);

          take F;

          thus thesis;

        end;

        

         A5: for F1,F2 be Function of ( Mor C), ( Ob C) holds (for f be Element of ( Mor C) holds (F1 . f) = ( dom f)) & (for f be Element of ( Mor C) holds (F2 . f) = ( dom f)) implies F1 = F2

        proof

          let F1,F2 be Function of ( Mor C), ( Ob C);

          assume

           A6: for f be Element of ( Mor C) holds (F1 . f) = ( dom f);

          assume

           A7: for f be Element of ( Mor C) holds (F2 . f) = ( dom f);

          for x be object st x in ( Mor C) holds (F1 . x) = (F2 . x)

          proof

            let x be object;

            assume x in ( Mor C);

            then

            reconsider f = x as Element of ( Mor C);

            

            thus (F1 . x) = ( dom f) by A6

            .= (F2 . x) by A7;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        thus thesis by A1, A4, A5;

      end;

      :: CAT_6:def31

      func TargetMap (C) -> Function of ( Mor C), ( Ob C) means

      : Def31: for f be Element of ( Mor C) holds (it . f) = ( cod f) if C is non empty

      otherwise it = {} ;

      correctness

      proof

        

         A8: not C is empty implies ex F be Function of ( Mor C), ( Ob C) st for f be Element of ( Mor C) holds (F . f) = ( cod f)

        proof

          assume not C is empty;

          then

          reconsider A = ( Mor C), O = ( Ob C) as non empty set;

          defpred P[ set, set] means ex a be Element of ( Mor C), o be Element of ( Ob C) st a = $1 & o = $2 & o = ( cod a);

          

           A9: for x be Element of A holds ex y be Element of O st P[x, y]

          proof

            let x be Element of A;

            reconsider f = x as Element of ( Mor C);

            reconsider y = ( cod f) as Element of O;

            take y;

            thus P[x, y];

          end;

          consider F be Function of A, O such that

           A10: for x be Element of A holds P[x, (F . x)] from FUNCT_2:sch 3( A9);

          reconsider F as Function of ( Mor C), ( Ob C);

          take F;

          let f be Element of ( Mor C);

           P[f, (F . f)] by A10;

          hence thesis;

        end;

        

         A11: C is empty implies ex F be Function of ( Mor C), ( Ob C) st F = {}

        proof

          assume C is empty;

          then ( Mor C) = {} & ( Ob C) = {} ;

          then

          reconsider F = {} as Function of ( Mor C), ( Ob C);

          take F;

          thus thesis;

        end;

        

         A12: for F1,F2 be Function of ( Mor C), ( Ob C) holds (for f be Element of ( Mor C) holds (F1 . f) = ( cod f)) & (for f be Element of ( Mor C) holds (F2 . f) = ( cod f)) implies F1 = F2

        proof

          let F1,F2 be Function of ( Mor C), ( Ob C);

          assume

           A13: for f be Element of ( Mor C) holds (F1 . f) = ( cod f);

          assume

           A14: for f be Element of ( Mor C) holds (F2 . f) = ( cod f);

          for x be object st x in ( Mor C) holds (F1 . x) = (F2 . x)

          proof

            let x be object;

            assume x in ( Mor C);

            then

            reconsider f = x as Element of ( Mor C);

            

            thus (F1 . x) = ( cod f) by A13

            .= (F2 . x) by A14;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        thus thesis by A8, A11, A12;

      end;

    end

    definition

      let C be with_identities CategoryStr;

      :: CAT_6:def32

      func IdMap (C) -> Function of ( Ob C), ( Mor C) means

      : Def32: for o be Element of ( Ob C) holds (it . o) = ( id- o) if C is non empty

      otherwise it = {} ;

      correctness

      proof

        

         A1: not C is empty implies ex F be Function of ( Ob C), ( Mor C) st for o be Element of ( Ob C) holds (F . o) = ( id- o)

        proof

          assume not C is empty;

          then

          reconsider A = ( Mor C), O = ( Ob C) as non empty set;

          defpred P[ set, set] means ex o be Element of ( Ob C), a be Element of ( Mor C) st o = $1 & a = $2 & a = ( id- o);

          

           A2: for x be Element of O holds ex y be Element of A st P[x, y]

          proof

            let x be Element of O;

            reconsider o = x as Element of ( Ob C);

            reconsider y = ( id- o) as Element of A;

            take y;

            thus P[x, y];

          end;

          consider F be Function of O, A such that

           A3: for x be Element of O holds P[x, (F . x)] from FUNCT_2:sch 3( A2);

          reconsider F as Function of ( Ob C), ( Mor C);

          take F;

          let o be Element of ( Ob C);

           P[o, (F . o)] by A3;

          hence thesis;

        end;

        

         A4: C is empty implies ex F be Function of ( Ob C), ( Mor C) st F = {}

        proof

          assume C is empty;

          then ( Mor C) = {} & ( Ob C) = {} ;

          then

          reconsider F = {} as Function of ( Ob C), ( Mor C);

          take F;

          thus thesis;

        end;

        

         A5: for F1,F2 be Function of ( Ob C), ( Mor C) holds (for o be Element of ( Ob C) holds (F1 . o) = ( id- o)) & (for o be Element of ( Ob C) holds (F2 . o) = ( id- o)) implies F1 = F2

        proof

          let F1,F2 be Function of ( Ob C), ( Mor C);

          assume

           A6: for o be Element of ( Ob C) holds (F1 . o) = ( id- o);

          assume

           A7: for o be Element of ( Ob C) holds (F2 . o) = ( id- o);

          for x be object st x in ( Ob C) holds (F1 . x) = (F2 . x)

          proof

            let x be object;

            assume x in ( Ob C);

            then

            reconsider o = x as Element of ( Ob C);

            

            thus (F1 . x) = ( id- o) by A6

            .= (F2 . x) by A7;

          end;

          hence thesis by FUNCT_2: 12;

        end;

        thus thesis by A1, A4, A5;

      end;

    end

    theorem :: CAT_6:36

    

     Th37: for C be non empty composable with_identities CategoryStr holds for f,g be Element of ( Mor C) holds [g, f] in ( dom ( CompMap C)) iff (( SourceMap C) . g) = (( TargetMap C) . f)

    proof

      let C be non empty composable with_identities CategoryStr;

      let f,g be Element of ( Mor C);

      hereby

        assume [g, f] in ( dom ( CompMap C));

        then

         A1: g |> f;

        consider u be morphism of C such that

         A2: ( dom g) = u & g |> u & u is identity by Def18;

        (g (*) u) = g by A2, Def5;

        then

         A3: u |> f by A2, A1, Lm3;

        

        thus (( SourceMap C) . g) = ( dom g) by Def30

        .= ( cod f) by A3, A2, Def19

        .= (( TargetMap C) . f) by Def31;

      end;

      assume

       A4: (( SourceMap C) . g) = (( TargetMap C) . f);

      

       A5: ( dom g) = (( SourceMap C) . g) by Def30

      .= ( cod f) by A4, Def31;

      consider d be morphism of C such that

       A6: ( dom g) = d & g |> d & d is identity by Def18;

      consider c be morphism of C such that

       A7: ( cod f) = c & c |> f & c is identity by Def19;

      (g (*) d) |> f by A6, A7, A5, Lm3;

      hence [g, f] in ( dom ( CompMap C)) by A6, Def5;

    end;

    theorem :: CAT_6:37

    

     Th38: for C be composable with_identities CategoryStr holds for f,g be Element of ( Mor C) st (( SourceMap C) . g) = (( TargetMap C) . f) holds (( SourceMap C) . (( CompMap C) . (g,f))) = (( SourceMap C) . f) & (( TargetMap C) . (( CompMap C) . (g,f))) = (( TargetMap C) . g)

    proof

      let C be composable with_identities CategoryStr;

      let f,g be Element of ( Mor C);

      assume

       A1: (( SourceMap C) . g) = (( TargetMap C) . f);

      per cases ;

        suppose

         A2: C is empty;

        

        thus (( SourceMap C) . (( CompMap C) . (g,f))) = {} by A2

        .= (( SourceMap C) . f) by A2;

        

        thus (( TargetMap C) . (( CompMap C) . (g,f))) = {} by A2

        .= (( TargetMap C) . g) by A2;

      end;

        suppose

         A3: not C is empty;

        then

         A4: [g, f] in ( dom ( CompMap C)) by A1, Th37;

        then

         A5: (( CompMap C) . [g, f]) in ( rng ( CompMap C)) by FUNCT_1: 3;

        reconsider a = (( CompMap C) . (g,f)) as Element of ( Mor C) by A5, BINOP_1:def 1;

        consider d be morphism of C such that

         A6: ( dom a) = d & a |> d & d is identity by A3, Def18;

        

         A7: g |> f by A4;

        

         A8: a = (the composition of C . [g, f]) by BINOP_1:def 1

        .= (g (*) f) by A4, Def2, Lm4;

        then f |> d by A6, A7, Lm3;

        then

         A9: ( dom a) = ( dom f) by A3, A6, Def18;

        

        thus (( SourceMap C) . (( CompMap C) . (g,f))) = ( dom a) by A3, Def30

        .= (( SourceMap C) . f) by A9, A3, Def30;

        consider c be morphism of C such that

         A10: ( cod a) = c & c |> a & c is identity by A3, Def19;

        c |> g by A10, A7, A8, Lm3;

        then

         A11: ( cod a) = ( cod g) by A3, A10, Def19;

        

        thus (( TargetMap C) . (( CompMap C) . (g,f))) = ( cod a) by A3, Def31

        .= (( TargetMap C) . g) by A11, A3, Def31;

      end;

    end;

    theorem :: CAT_6:38

    

     Th39: for C be composable associative with_identities CategoryStr holds for f,g,h be Element of ( Mor C) st (( SourceMap C) . h) = (( TargetMap C) . g) & (( SourceMap C) . g) = (( TargetMap C) . f) holds (( CompMap C) . (h,(( CompMap C) . (g,f)))) = (( CompMap C) . ((( CompMap C) . (h,g)),f))

    proof

      let C be composable associative with_identities CategoryStr;

      let f,g,h be Element of ( Mor C);

      assume

       A1: (( SourceMap C) . h) = (( TargetMap C) . g) & (( SourceMap C) . g) = (( TargetMap C) . f);

      per cases ;

        suppose

         A2: C is empty;

        

        thus (( CompMap C) . (h,(( CompMap C) . (g,f)))) = (( CompMap C) . [h, (( CompMap C) . (g,f))]) by BINOP_1:def 1

        .= {} by A2

        .= (( CompMap C) . [(( CompMap C) . (h,g)), f]) by A2

        .= (( CompMap C) . ((( CompMap C) . (h,g)),f)) by BINOP_1:def 1;

      end;

        suppose

         A3: not C is empty;

        

         A4: [h, g] in ( dom ( CompMap C)) by Th37, A3, A1;

        then

         A5: h |> g;

        

         A6: [g, f] in ( dom ( CompMap C)) by Th37, A3, A1;

        then

         A7: g |> f;

        

         A8: h |> (g (*) f) by A7, A5, Lm3;

        

         A9: (h (*) g) |> f by A7, A5, Lm3;

        

         A10: (( CompMap C) . (g,f)) = (the composition of C . [g, f]) by BINOP_1:def 1

        .= (g (*) f) by A6, Def2, Lm4;

        

         A11: (( CompMap C) . (h,g)) = (the composition of C . [h, g]) by BINOP_1:def 1

        .= (h (*) g) by A4, Def2, Lm4;

        

        thus (( CompMap C) . (h,(( CompMap C) . (g,f)))) = (( CompMap C) . [h, (g (*) f)]) by A10, BINOP_1:def 1

        .= (h (*) (g (*) f)) by A8, Lm4

        .= ((h (*) g) (*) f) by A5, A7, Lm5

        .= (( CompMap C) . [(h (*) g), f]) by A9, Lm4

        .= (( CompMap C) . ((( CompMap C) . (h,g)),f)) by A11, BINOP_1:def 1;

      end;

    end;

    theorem :: CAT_6:39

    

     Th40: for C be composable with_identities CategoryStr holds for b be Element of ( Ob C) holds (( SourceMap C) . (( IdMap C) . b)) = b & (( TargetMap C) . (( IdMap C) . b)) = b & (for f be Element of ( Mor C) st (( TargetMap C) . f) = b holds (( CompMap C) . ((( IdMap C) . b),f)) = f) & for g be Element of ( Mor C) st (( SourceMap C) . g) = b holds (( CompMap C) . (g,(( IdMap C) . b))) = g

    proof

      let C be composable with_identities CategoryStr;

      let b be Element of ( Ob C);

      per cases ;

        suppose

         A1: C is empty;

        then

         A2: b = {} by SUBSET_1:def 1;

        thus (( SourceMap C) . (( IdMap C) . b)) = b by A1, A2;

        thus (( TargetMap C) . (( IdMap C) . b)) = b by A1, A2;

        thus for f be Element of ( Mor C) st (( TargetMap C) . f) = b holds (( CompMap C) . ((( IdMap C) . b),f)) = f

        proof

          let f be Element of ( Mor C);

          assume (( TargetMap C) . f) = b;

          

           A3: f = {} by A1, SUBSET_1:def 1;

          

          thus (( CompMap C) . ((( IdMap C) . b),f)) = (the composition of C . [(( IdMap C) . b), f]) by BINOP_1:def 1

          .= f by A1, A3;

        end;

        thus for g be Element of ( Mor C) st (( SourceMap C) . g) = b holds (( CompMap C) . (g,(( IdMap C) . b))) = g

        proof

          let g be Element of ( Mor C);

          assume (( SourceMap C) . g) = b;

          

           A4: g = {} by A1, SUBSET_1:def 1;

          

          thus (( CompMap C) . (g,(( IdMap C) . b))) = (the composition of C . [g, (( IdMap C) . b)]) by BINOP_1:def 1

          .= g by A1, A4;

        end;

      end;

        suppose

         A5: not C is empty;

        

        then

         A6: (( IdMap C) . b) = ( id- b) by Def32

        .= b;

         not ( Ob C) is empty by A5;

        then b in ( Ob C);

        then

        reconsider u = b as Element of ( Mor C);

        

         A7: u is identity by A5, Th22;

        consider d be morphism of C such that

         A8: ( dom u) = d & u |> d & d is identity by A5, Def18;

        

         A9: d = (u (*) d) by A7, A8, Def4

        .= u by A8, Def5;

        thus

         A10: (( SourceMap C) . (( IdMap C) . b)) = b by A8, A9, A6, A5, Def30;

        consider c be morphism of C such that

         A11: ( cod u) = c & c |> u & c is identity by A5, Def19;

        

         A12: c = (c (*) u) by A7, A11, Def5

        .= u by A11, Def4;

        thus

         A13: (( TargetMap C) . (( IdMap C) . b)) = b by A11, A12, A6, A5, Def31;

        thus for f be Element of ( Mor C) st (( TargetMap C) . f) = b holds (( CompMap C) . ((( IdMap C) . b),f)) = f

        proof

          let f be Element of ( Mor C);

          assume (( TargetMap C) . f) = b;

          then

           A14: [u, f] in ( dom ( CompMap C)) by A6, A10, A5, Th37;

          then

           A15: u |> f;

          

          thus (( CompMap C) . ((( IdMap C) . b),f)) = (( CompMap C) . [u, f]) by A6, BINOP_1:def 1

          .= (u (*) f) by A14, Def2, Lm4

          .= f by A7, A15, Def4;

        end;

        thus for g be Element of ( Mor C) st (( SourceMap C) . g) = b holds (( CompMap C) . (g,(( IdMap C) . b))) = g

        proof

          let g be Element of ( Mor C);

          assume (( SourceMap C) . g) = b;

          then

           A16: [g, u] in ( dom ( CompMap C)) by A6, A13, A5, Th37;

          then

           A17: g |> u;

          

          thus (( CompMap C) . (g,(( IdMap C) . b))) = (( CompMap C) . [g, u]) by A6, BINOP_1:def 1

          .= (g (*) u) by A16, Def2, Lm4

          .= g by A7, A17, Def5;

        end;

      end;

    end;

    

     Lm6: for C be non empty category holds CatStr (# ( Ob C), ( Mor C), ( SourceMap C), ( TargetMap C), ( CompMap C) #) is Category

    proof

      let C be non empty composable associative with_identities CategoryStr;

      set CC = CatStr (# ( Ob C), ( Mor C), ( SourceMap C), ( TargetMap C), ( CompMap C) #);

      reconsider CC as non empty non void CatStr;

      

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

      proof

        let f,g be Morphism of CC;

        (the Source of CC . g) = ( dom g) & (the Target of CC . f) = ( cod f) by GRAPH_1:def 4, GRAPH_1:def 3;

        hence thesis by Th37;

      end;

      

       A2: for f,g be Morphism of CC st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g)

      proof

        let f,g be Morphism of CC;

        assume

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

        

        then

         A4: (the Source of CC . g) = ( cod f) by GRAPH_1:def 3

        .= (the Target of CC . f) by GRAPH_1:def 4;

        

         A5: [g, f] in ( dom the Comp of CC) by A3, A1;

        

        thus ( dom (g (*) f)) = (the Source of CC . (g (*) f)) by GRAPH_1:def 3

        .= (the Source of CC . (the Comp of CC . (g,f))) by A5, CAT_1:def 1

        .= (the Source of CC . f) by A4, Th38

        .= ( dom f) by GRAPH_1:def 3;

        

        thus ( cod (g (*) f)) = (the Target of CC . (g (*) f)) by GRAPH_1:def 4

        .= (the Target of CC . (the Comp of CC . (g,f))) by A5, CAT_1:def 1

        .= (the Target of CC . g) by A4, Th38

        .= ( cod g) by GRAPH_1:def 4;

      end;

      

       A6: for f,g,h be Morphism of CC st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

      proof

        let f,g,h be Morphism of CC;

        assume

         A7: ( dom h) = ( cod g);

        

        then

         A8: (the Source of CC . h) = ( cod g) by GRAPH_1:def 3

        .= (the Target of CC . g) by GRAPH_1:def 4;

        

         A9: [h, g] in ( dom the Comp of CC) by A7, A1;

        assume

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

        

        then

         A11: (the Source of CC . g) = ( cod f) by GRAPH_1:def 3

        .= (the Target of CC . f) by GRAPH_1:def 4;

        

         A12: [g, f] in ( dom the Comp of CC) by A10, A1;

        ( dom h) = ( cod (g (*) f)) by A2, A7, A10;

        then

         A13: [h, (g (*) f)] in ( dom the Comp of CC) by A1;

        ( dom (h (*) g)) = ( cod f) by A2, A7, A10;

        then

         A14: [(h (*) g), f] in ( dom the Comp of CC) by A1;

        

        thus (h (*) (g (*) f)) = (the Comp of CC . (h,(g (*) f))) by A13, CAT_1:def 1

        .= (the Comp of CC . (h,(the Comp of CC . (g,f)))) by A12, CAT_1:def 1

        .= (the Comp of CC . ((the Comp of CC . (h,g)),f)) by Th39, A8, A11

        .= (the Comp of CC . ((h (*) g),f)) by A9, CAT_1:def 1

        .= ((h (*) g) (*) f) by A14, CAT_1:def 1;

      end;

      

       A15: for b be Element of CC holds (( IdMap C) . b) in ( Hom (b,b))

      proof

        let b be Element of CC;

        reconsider o = b as Element of ( Ob C);

        reconsider f = o as Morphism of CC by TARSKI:def 3;

        

         A16: (( IdMap C) . b) = ( id- o) by Def32

        .= f;

        (( SourceMap C) . (( IdMap C) . b)) = b & (( TargetMap C) . (( IdMap C) . b)) = b by Th40;

        then (( SourceMap C) . ( id- o)) = b & (( TargetMap C) . ( id- o)) = b by Def32;

        then ( dom f) = b & ( cod f) = b by GRAPH_1:def 3, GRAPH_1:def 4;

        hence (( IdMap C) . b) in ( Hom (b,b)) by A16, CAT_1: 1;

      end;

      then

       A17: for b be Element of CC holds ( Hom (b,b)) <> {} ;

      for a be Element of CC holds ex i be Morphism of a, a st for b be Element of CC 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 CC;

        set i = (( IdMap C) . a);

        

         A18: i in ( Hom (a,a)) by A15;

        then

        reconsider i as Morphism of a, a by CAT_1:def 5;

        take i;

        let b be Element of CC;

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

        proof

          assume

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

          let g be Morphism of a, b;

          g in ( Hom (a,b)) by A19, CAT_1:def 5;

          then

           A20: ( dom g) = a by CAT_1: 1;

          then ( dom g) = ( cod i) by A18, CAT_1: 1;

          then

           A21: [g, i] in ( dom the Comp of CC) by A1;

          (the Source of CC . g) = a by A20, GRAPH_1:def 3;

          then (( CompMap C) . (g,(( IdMap C) . a))) = g by Th40;

          hence (g (*) i) = g by A21, CAT_1:def 1;

        end;

        assume

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

        let f be Morphism of b, a;

        f in ( Hom (b,a)) by A22, CAT_1:def 5;

        then

         A23: ( cod f) = a by CAT_1: 1;

        then ( cod f) = ( dom i) by A18, CAT_1: 1;

        then

         A24: [i, f] in ( dom the Comp of CC) by A1;

        (the Target of CC . f) = a by A23, GRAPH_1:def 4;

        then (( CompMap C) . ((( IdMap C) . a),f)) = f by Th40;

        hence (i (*) f) = f by A24, CAT_1:def 1;

      end;

      hence thesis by A1, A2, A6, A17, CAT_1:def 6, CAT_1:def 7, CAT_1:def 8, CAT_1:def 9, CAT_1:def 10;

    end;

    definition

      let C be non empty category;

      :: CAT_6:def33

      func Alter (C) -> strict Category equals CatStr (# ( Ob C), ( Mor C), ( SourceMap C), ( TargetMap C), ( CompMap C) #);

      coherence by Lm6;

    end

    

     Lm7: for C be Category holds CategoryStr (# the carrier' of C, the Comp of C #) is category

    proof

      let C be Category;

      consider o be object such that

       A1: o in the carrier of C by XBOOLE_0:def 1;

      reconsider o as Object of C by A1;

      reconsider cc = CategoryStr (# the carrier' of C, the Comp of C #) as non empty CategoryStr;

      

       A2: for f,g be morphism of cc, f1,g1 be Element of the carrier' of C st g = g1 & f = f1 & g |> f holds (g (*) f) = (g1 (*) f1)

      proof

        let f,g be morphism of cc;

        let f1,g1 be Element of the carrier' of C;

        assume

         A3: g = g1 & f = f1;

        assume

         A4: g |> f;

        

        thus (g (*) f) = (( CompMap cc) . [g1, f1]) by A3, A4, Lm4

        .= (the Comp of C . (g1,f1)) by BINOP_1:def 1

        .= (g1 (*) f1) by A3, A4, CAT_1:def 1;

      end;

      

       A5: for f,g,h be morphism of cc holds ((h (*) g) |> f & h |> g implies g |> f) & (h |> (g (*) f) & g |> f implies h |> g) & (g |> f & h |> g implies (h (*) g) |> f & h |> (g (*) f))

      proof

        let f,g,h be morphism of cc;

        reconsider f1 = f, g1 = g, h1 = h as Morphism of C;

        thus ((h (*) g) |> f & h |> g implies g |> f)

        proof

          assume

           A6: (h (*) g) |> f;

          assume

           A7: h |> g;

          then

           A8: ( dom h1) = ( cod g1) by CAT_1:def 6;

          (h (*) g) = (h1 (*) g1) by A7, A2;

          then ( dom (h1 (*) g1)) = ( cod f1) by A6, CAT_1:def 6;

          then ( dom g1) = ( cod f1) by A8, CAT_1:def 7;

          hence g |> f by CAT_1:def 6;

        end;

        thus (h |> (g (*) f) & g |> f implies h |> g)

        proof

          assume

           A9: h |> (g (*) f);

          assume

           A10: g |> f;

          then

           A11: ( dom g1) = ( cod f1) by CAT_1:def 6;

          (g (*) f) = (g1 (*) f1) by A10, A2;

          then ( dom h1) = ( cod (g1 (*) f1)) by A9, CAT_1:def 6;

          then ( dom h1) = ( cod g1) by A11, CAT_1:def 7;

          hence h |> g by CAT_1:def 6;

        end;

        assume

         A12: g |> f;

        then

         A13: ( dom g1) = ( cod f1) by CAT_1:def 6;

        assume

         A14: h |> g;

        

         A15: ( dom h1) = ( cod g1) by A14, CAT_1:def 6;

        ( dom (h1 (*) g1)) = ( cod f1) by A13, A15, CAT_1:def 7;

        then [(h1 (*) g1), f1] in ( dom ( CompMap cc)) by CAT_1:def 6;

        hence (h (*) g) |> f by A14, A2;

        ( dom h1) = ( cod g1) by A14, CAT_1:def 6;

        then ( dom h1) = ( cod (g1 (*) f1)) by A13, CAT_1:def 7;

        then [h1, (g1 (*) f1)] in ( dom ( CompMap cc)) by CAT_1:def 6;

        hence h |> (g (*) f) by A12, A2;

      end;

      

       A16: for f,g,h be morphism of cc st h |> g & g |> f holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

      proof

        let f,g,h be morphism of cc;

        reconsider f1 = f, g1 = g, h1 = h, gf1 = (g (*) f), hg1 = (h (*) g) as Morphism of C;

        assume

         A17: h |> g;

        then

         A18: ( dom h1) = ( cod g1) by CAT_1:def 6;

        assume

         A19: g |> f;

        then

         A20: ( dom g1) = ( cod f1) by CAT_1:def 6;

        

         A21: h |> (g (*) f) by A17, A19, A5;

        

         A22: (h (*) g) |> f by A17, A19, A5;

        

        thus (h (*) (g (*) f)) = (h1 (*) gf1) by A21, A2

        .= (h1 (*) (g1 (*) f1)) by A19, A2

        .= ((h1 (*) g1) (*) f1) by A20, A18, CAT_1:def 8

        .= (hg1 (*) f1) by A17, A2

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

      end;

      

       A23: for f be morphism of cc st f in ( Mor cc) holds (ex c be morphism of cc st c |> f & c is identity) & (ex d be morphism of cc st f |> d & d is identity)

      proof

        let f be morphism of cc;

        assume f in ( Mor cc);

        reconsider f1 = f as Morphism of C;

        thus (ex c be morphism of cc st c |> f & c is identity)

        proof

          set c1 = ( id ( cod f1));

          

           A24: ( dom c1) = ( cod f1);

          reconsider c = c1 as morphism of cc;

          take c;

          thus c |> f by A24, CAT_1:def 6;

          

           A25: for ff be morphism of cc st c |> ff holds (c (*) ff) = ff

          proof

            let ff be morphism of cc;

            reconsider ff1 = ff as Morphism of C;

            assume

             A26: c |> ff;

            then

             A27: ( dom c1) = ( cod ff1) by CAT_1:def 6;

            

            thus (c (*) ff) = (c1 (*) ff1) by A26, A2

            .= ff by A27, CAT_1: 21;

          end;

          for gg be morphism of cc st gg |> c holds (gg (*) c) = gg

          proof

            let gg be morphism of cc;

            reconsider gg1 = gg as Morphism of C;

            assume

             A28: gg |> c;

            then

             A29: ( cod c1) = ( dom gg1) by CAT_1:def 6;

            

            thus (gg (*) c) = (gg1 (*) c1) by A28, A2

            .= gg by A29, CAT_1: 22;

          end;

          hence c is identity by A25, Def4, Def5;

        end;

        set d1 = ( id ( dom f1));

        

         A30: ( cod d1) = ( dom f1);

        reconsider d = d1 as morphism of cc;

        take d;

        thus f |> d by A30, CAT_1:def 6;

        

         A31: for ff be morphism of cc st d |> ff holds (d (*) ff) = ff

        proof

          let ff be morphism of cc;

          reconsider ff1 = ff as Morphism of C;

          assume

           A32: d |> ff;

          then

           A33: ( dom d1) = ( cod ff1) by CAT_1:def 6;

          

          thus (d (*) ff) = (d1 (*) ff1) by A32, A2

          .= ff by A33, CAT_1: 21;

        end;

        for gg be morphism of cc st gg |> d holds (gg (*) d) = gg

        proof

          let gg be morphism of cc;

          reconsider gg1 = gg as Morphism of C;

          assume

           A34: gg |> d;

          then

           A35: ( cod d1) = ( dom gg1) by CAT_1:def 6;

          

          thus (gg (*) d) = (gg1 (*) d1) by A34, A2

          .= gg by A35, CAT_1: 22;

        end;

        hence d is identity by A31, Def4, Def5;

      end;

      set CS = CategoryStr (# the carrier' of C, the Comp of C #);

      CS is composable by A5, Lm3;

      hence thesis by A23, A16, Lm5, Lm2;

    end;

    definition

      let A be Category;

      :: CAT_6:def34

      func alter (A) -> strict category equals CategoryStr (# the carrier' of A, the Comp of A #);

      coherence by Lm7;

    end

    registration

      let A be Category;

      cluster ( alter A) -> non empty;

      correctness ;

    end

    theorem :: CAT_6:40

    

     Th41: for A be Category, a1,a2 be Morphism of A, f1,f2 be morphism of ( alter A) st a1 = f1 & a2 = f2 & [a1, a2] in ( dom the Comp of A) holds (a1 (*) a2) = (f1 (*) f2)

    proof

      let A be Category;

      let a1,a2 be Morphism of A;

      let f1,f2 be morphism of ( alter A);

      assume

       A1: a1 = f1 & a2 = f2;

      assume

       A2: [a1, a2] in ( dom the Comp of A);

      

      thus (a1 (*) a2) = (the composition of ( alter A) . (f1,f2)) by A1, A2, CAT_1:def 1

      .= (f1 (*) f2) by A2, A1, Def2, Def3;

    end;

    theorem :: CAT_6:41

    

     Th42: for A be Category, f be morphism of ( alter A) holds f is identity iff ex o be Object of A st f = ( id o)

    proof

      let A be Category;

      let f be morphism of ( alter A);

      hereby

        assume

         A1: f is identity;

        

         A3: f is Object of ( alter A) by A1, Th22;

        then

         A4: for f1 be morphism of ( alter A) holds (f |> f1 implies (f (*) f1) = f1) & (f1 |> f implies (f1 (*) f) = f1) & f |> f by Th23;

        reconsider a1 = f as Morphism of A;

         [a1, a1] in ( dom the Comp of A) by A4, Def2;

        then

         A5: ( dom a1) = ( cod a1) by CAT_1: 15;

        set o = ( dom a1);

        reconsider a1 as Morphism of o, o by A5, CAT_1: 4;

        take o;

        for b be Object of A holds (( Hom (o,b)) <> {} implies for a be Morphism of o, b holds (a (*) a1) = a) & (( Hom (b,o)) <> {} implies for a be Morphism of b, o holds (a1 (*) a) = a)

        proof

          let b be Object of A;

          thus (( Hom (o,b)) <> {} implies for f1 be Morphism of o, b holds (f1 (*) a1) = f1)

          proof

            assume

             A6: ( Hom (o,b)) <> {} ;

            let f1 be Morphism of o, b;

            f1 in ( Hom (o,b)) by A6, CAT_1:def 5;

            then ( dom f1) = o & ( cod f1) = b by CAT_1: 1;

            then

             A7: [f1, a1] in ( dom the Comp of A) by A5, CAT_1:def 6;

            reconsider f2 = f1 as morphism of ( alter A);

            (f2 (*) f) = f2 by A4, A7, Def2;

            hence (f1 (*) a1) = f1 by Th41, A7;

          end;

          assume

           A8: ( Hom (b,o)) <> {} ;

          let f1 be Morphism of b, o;

          f1 in ( Hom (b,o)) by A8, CAT_1:def 5;

          then

           A9: ( dom f1) = b & ( cod f1) = o by CAT_1: 1;

          then

           A10: [a1, f1] in ( dom the Comp of A) by CAT_1:def 6;

          reconsider f2 = f1 as morphism of ( alter A);

          f |> f2 by A9, CAT_1:def 6;

          then (f (*) f2) = f2 by A3, Th23;

          hence (a1 (*) f1) = f1 by Th41, A10;

        end;

        hence f = ( id o) by CAT_1:def 12;

      end;

      given o be Object of A such that

       A11: f = ( id o);

      

       A12: for f1 be morphism of ( alter A) st f |> f1 holds (f (*) f1) = f1

      proof

        let f1 be morphism of ( alter A);

        assume

         A13: f |> f1;

        reconsider a2 = f1, a1 = f as Morphism of A;

        

         A14: ( cod a2) = ( dom ( id o)) by A11, CAT_1: 15, A13

        .= o;

        

        thus (f (*) f1) = (a1 (*) a2) by A13, Th41

        .= f1 by A11, A14, CAT_1: 21;

      end;

      for f1 be morphism of ( alter A) st f1 |> f holds (f1 (*) f) = f1

      proof

        let f1 be morphism of ( alter A);

        assume

         A15: f1 |> f;

        reconsider a2 = f1, a1 = f as Morphism of A;

        

         A16: ( dom a2) = ( cod ( id o)) by A15, A11, CAT_1: 15

        .= o;

        

        thus (f1 (*) f) = (a2 (*) a1) by A15, Th41

        .= f1 by A11, A16, CAT_1: 22;

      end;

      then f is right_identity;

      hence f is identity by A12, Def4;

    end;

    theorem :: CAT_6:42

    for A,B be Category, F be Functor of A, B holds F is covariant Functor of ( alter A), ( alter B)

    proof

      let A,B be Category;

      let F be Functor of A, B;

      reconsider F1 = F as Function of ( alter A), ( alter B);

      for f1,f2 be morphism of ( alter A) st f1 |> f2 holds (F1 . f1) |> (F1 . f2) & (F1 . (f1 (*) f2)) = ((F1 . f1) (*) (F1 . f2))

      proof

        let f1,f2 be morphism of ( alter A);

        assume

         A1: f1 |> f2;

        reconsider a1 = f1, a2 = f2 as Morphism of A;

        

         A2: ( dom a1) = ( cod a2) by A1, CAT_1: 15;

        ( dom (F . a1)) = (F . ( dom a1)) & ( cod (F . a2)) = (F . ( cod a2)) by CAT_1: 72;

        then ( dom (F . a1)) = ( cod (F . a2)) by A1, CAT_1: 15;

        then

         A3: [(F . a1), (F . a2)] in ( dom the Comp of B) by CAT_1: 15;

        

         A4: (F1 . f1) = (F . a1) by Def21;

        

         A5: (F1 . f2) = (F . a2) by Def21;

        thus ((F1 . f1),(F1 . f2)) are_composable by A3, A4, Def21;

        (f1 (*) f2) = (a1 (*) a2) by A1, Th41;

        

        hence (F1 . (f1 (*) f2)) = (F . (a1 (*) a2)) by Def21

        .= ((F . a1) (*) (F . a2)) by A2, CAT_1: 64

        .= ((F1 . f1) (*) (F1 . f2)) by A3, A4, A5, Th41;

      end;

      then

       A6: F1 is multiplicative;

      for f be morphism of ( alter A) st f is identity holds (F1 . f) is identity

      proof

        let f be morphism of ( alter A);

        assume f is identity;

        then

        consider o be Object of A such that

         A7: f = ( id o) by Th42;

        consider o1 be Object of B such that

         A8: (F . ( id o)) = ( id o1) by CAT_1: 62;

        thus (F1 . f) is identity by Def21, A7, A8, Th42;

      end;

      hence thesis by A6, Def25, Def22;

    end;

    theorem :: CAT_6:43

    

     Th44: for C be non empty category, a1,a2 be Morphism of ( Alter C), f1,f2 be morphism of C st a1 = f1 & a2 = f2 & f1 |> f2 holds (a1 (*) a2) = (f1 (*) f2)

    proof

      let C be non empty category;

      let a1,a2 be Morphism of ( Alter C);

      let f1,f2 be morphism of C;

      assume

       A1: a1 = f1 & a2 = f2;

      assume

       A2: f1 |> f2;

      

      thus (a1 (*) a2) = (the Comp of ( Alter C) . (a1,a2)) by A1, A2, CAT_1:def 1

      .= (f1 (*) f2) by A1, A2, Def3;

    end;

    theorem :: CAT_6:44

    

     Th45: for C be non empty category, f1 be morphism of C, a1 be Morphism of ( Alter C) st a1 = f1 holds ( dom f1) = ( dom a1) & ( cod f1) = ( cod a1)

    proof

      let C be non empty category;

      let f1 be morphism of C;

      let a1 be Morphism of ( Alter C);

      assume

       A1: a1 = f1;

      

      thus ( dom f1) = (the Source of ( Alter C) . a1) by A1, Def30

      .= ( dom a1) by GRAPH_1:def 3;

      

      thus ( cod f1) = (the Target of ( Alter C) . a1) by A1, Def31

      .= ( cod a1) by GRAPH_1:def 4;

    end;

    theorem :: CAT_6:45

    

     Th46: for C be non empty category, o1 be Object of C, o2 be Object of ( Alter C) st o1 = o2 holds ( id- o1) = ( id o2)

    proof

      let C be non empty category;

      let o1 be Object of C;

      let o2 be Object of ( Alter C);

      assume

       A1: o1 = o2;

      

       A2: o1 in ( Ob C);

      then

      reconsider f1 = o1 as morphism of C;

      reconsider a2 = o2 as Morphism of ( Alter C) by A1, A2;

      

       A3: f1 is identity & f1 |> f1 by Th22, Th24;

      

       A4: ( dom a2) = ( dom f1) by A1, Th45

      .= o2 by A1, A3, Def18;

      

       A5: ( cod a2) = ( cod f1) by A1, Th45

      .= o2 by A1, A3, Def19;

      reconsider a3 = a2 as Morphism of o2, o2 by A4, A5, CAT_1: 4;

      for b be Object of ( Alter C) holds (( Hom (o2,b)) <> {} implies for a be Morphism of o2, b holds (a (*) a3) = a) & (( Hom (b,o2)) <> {} implies for a be Morphism of b, o2 holds (a3 (*) a) = a)

      proof

        let b be Object of ( Alter C);

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

        proof

          assume

           A6: ( Hom (o2,b)) <> {} ;

          let a be Morphism of o2, b;

          reconsider f2 = a as morphism of C;

          ( dom a) = ( cod a3) by A5, A6, CAT_1: 5;

          then

           A7: [f2, f1] in ( dom the composition of C) by A1, CAT_1: 15;

          

          thus (a (*) a3) = (f2 (*) f1) by A1, A7, Def2, Th44

          .= a by A3, A7, Def2, Def5;

        end;

        assume

         A8: ( Hom (b,o2)) <> {} ;

        let a be Morphism of b, o2;

        reconsider f2 = a as morphism of C;

        ( dom a3) = ( cod a) by A4, A8, CAT_1: 5;

        then

         A9: [f1, f2] in ( dom the composition of C) by A1, CAT_1: 15;

        

        thus (a3 (*) a) = (f1 (*) f2) by A1, A9, Def2, Th44

        .= a by A3, A9, Def2, Def4;

      end;

      hence thesis by A1, CAT_1:def 12;

    end;

    theorem :: CAT_6:46

    

     Th47: for C be non empty category, f be morphism of C holds f is identity iff ex o be Object of ( Alter C) st f = ( id o)

    proof

      let C be non empty category;

      let f be morphism of C;

      set A = ( Alter C);

      reconsider a = f as morphism of ( alter A);

      hereby

        assume f is identity;

        then a is identity by Th25;

        then

        consider o be Object of ( Alter C) such that

         A1: a = ( id o) by Th42;

        take o;

        thus f = ( id o) by A1;

      end;

      given o be Object of ( Alter C) such that

       A2: f = ( id o);

      a is identity by A2, Th42;

      hence f is identity by Th25;

    end;

    theorem :: CAT_6:47

    for C,D be non empty category, F be covariant Functor of C, D holds F is Functor of ( Alter C), ( Alter D)

    proof

      let C,D be non empty category;

      let F be covariant Functor of C, D;

      reconsider F1 = F as Function of the carrier' of ( Alter C), the carrier' of ( Alter D);

      

       A1: F is identity-preserving & F is multiplicative by Def25;

      

       A2: for a be Object of ( Alter C) holds ex b be Object of ( Alter D) st (F1 . ( id a)) = ( id b)

      proof

        let a be Object of ( Alter C);

        reconsider a1 = ( id a) as morphism of C;

        a1 is identity by Th47;

        then

        consider b be Object of ( Alter D) such that

         A3: (F . a1) = ( id b) by Th47, A1;

        take b;

        thus (F1 . ( id a)) = ( id b) by A3, Def21;

      end;

      

       A4: for f be Morphism of ( Alter C) holds (F1 . ( id ( dom f))) = ( id ( dom (F1 . f))) & (F1 . ( id ( cod f))) = ( id ( cod (F1 . f)))

      proof

        let f be Morphism of ( Alter C);

        reconsider o1 = ( dom f) as Object of ( Alter C);

        reconsider o2 = o1 as Object of C;

        reconsider f1 = f as morphism of C;

        

         A5: (F . f1) = (F1 . f) by Def21;

        

         A6: (F . o2) = (F1 . ( dom f1)) by Th45

        .= ( dom (F . f1)) by Th32

        .= ( dom (F1 . f)) by Th45, A5;

        

        thus (F1 . ( id ( dom f))) = (F1 . ( id- o2)) by Th46

        .= ( id- (F . o2))

        .= ( id ( dom (F1 . f))) by A6, Th46;

        reconsider o3 = ( cod f) as Object of ( Alter C);

        reconsider o4 = o3 as Object of C;

        reconsider f1 = f as morphism of C;

        

         A7: (F . f1) = (F1 . f) by Def21;

        

         A8: (F . o3) = (F1 . ( cod f1)) by Th45

        .= ( cod (F . f1)) by Th32

        .= ( cod (F1 . f)) by Th45, A7;

        

        thus (F1 . ( id ( cod f))) = (F1 . ( id- o4)) by Th46

        .= ( id- (F . o4))

        .= ( id ( cod (F1 . f))) by A8, Th46;

      end;

      for f,g be Morphism of ( Alter C) st ( dom g) = ( cod f) holds (F1 . (g (*) f)) = ((F1 . g) (*) (F1 . f))

      proof

        let f,g be Morphism of ( Alter C);

        assume

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

        reconsider f1 = f, g1 = g as morphism of C;

        

         A10: [g1, f1] in ( dom the composition of C) by A9, CAT_1: 15;

        

         A11: g1 |> f1 by A9, CAT_1: 15;

        

         A12: (the composition of C . (g1,f1)) = (g1 (*) f1) by A10, Def2, Def3;

        

         A13: (F . g1) = (F1 . g) & (F . f1) = (F1 . f) by Def21;

        

         A14: [(F1 . g), (F1 . f)] in ( dom the Comp of ( Alter D)) by A13, Def2, A11, A1;

        

        thus (F1 . (g (*) f)) = (F1 . (the Comp of ( Alter C) . (g,f))) by A9, CAT_1: 16

        .= (F . (g1 (*) f1)) by A12, Def21

        .= ((F . g1) (*) (F . f1)) by A11, A1

        .= (the Comp of ( Alter D) . ((F1 . g),(F1 . f))) by A13, Def3, A11, A1

        .= ((F1 . g) (*) (F1 . f)) by A14, CAT_1:def 1;

      end;

      hence thesis by A2, A4, CAT_1: 61;

    end;

    theorem :: CAT_6:48

    

     Th49: for C,D be Category, F be covariant Functor of ( alter C), ( alter D) holds F is Functor of C, D

    proof

      let C,D be Category;

      let F be covariant Functor of ( alter C), ( alter D);

      reconsider F1 = F as Function of the carrier' of C, the carrier' of D;

      

       A1: F is identity-preserving & F is multiplicative by Def25;

      

       A2: for a be Object of C holds ex b be Object of D st (F1 . ( id a)) = ( id b)

      proof

        let a be Object of C;

        reconsider a1 = ( id a) as morphism of ( alter C);

        a1 is identity by Th42;

        then

        consider b be Object of D such that

         A3: (F . a1) = ( id b) by Th42, A1;

        take b;

        thus (F1 . ( id a)) = ( id b) by A3, Def21;

      end;

      

       A4: for f be Morphism of C holds (F1 . ( id ( dom f))) = ( id ( dom (F1 . f))) & (F1 . ( id ( cod f))) = ( id ( cod (F1 . f)))

      proof

        let f be Morphism of C;

        reconsider f1 = f as morphism of ( alter C);

        reconsider d1 = ( id ( dom f)) as morphism of ( alter C);

        ( dom f) = ( cod ( id ( dom f)));

        then

         A5: f1 |> d1 by CAT_1: 15;

        

         A6: (F . d1) is identity by Th42, A1;

        reconsider d2 = ( id ( dom (F1 . f))) as morphism of ( alter D);

        ( dom (F1 . f)) = ( cod ( id ( dom (F1 . f))));

        then [(F1 . f), ( id ( dom (F1 . f)))] in ( dom the Comp of D) by CAT_1: 15;

        then

         A7: (F . f1) |> d2 by Def21;

        (F . d1) = ( dom (F . f1)) by A1, A5, A6, Th26

        .= d2 by Th42, A7, Th26;

        hence (F1 . ( id ( dom f))) = ( id ( dom (F1 . f))) by Def21;

        reconsider c1 = ( id ( cod f)) as morphism of ( alter C);

        ( cod f) = ( dom ( id ( cod f)));

        then

         A8: c1 |> f1 by CAT_1: 15;

        

         A9: (F . c1) is identity by Th42, A1;

        reconsider c2 = ( id ( cod (F1 . f))) as morphism of ( alter D);

        ( cod (F1 . f)) = ( dom ( id ( cod (F1 . f))));

        then [( id ( cod (F1 . f))), (F1 . f)] in ( dom the Comp of D) by CAT_1: 15;

        then

         A10: c2 |> (F . f1) by Def21;

        (F . c1) = ( cod (F . f1)) by A1, A8, A9, Th27

        .= c2 by Th42, A10, Th27;

        hence (F1 . ( id ( cod f))) = ( id ( cod (F1 . f))) by Def21;

      end;

      for f,g be Morphism of C st ( dom g) = ( cod f) holds (F1 . (g (*) f)) = ((F1 . g) (*) (F1 . f))

      proof

        let f,g be Morphism of C;

        assume

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

        reconsider f1 = f, g1 = g as morphism of ( alter C);

        

         A12: [g1, f1] in ( dom the composition of ( alter C)) by A11, CAT_1: 15;

        

         A13: g1 |> f1 by A11, CAT_1: 15;

        

         A14: (the composition of ( alter C) . (g1,f1)) = (g1 (*) f1) by A12, Def2, Def3;

        

         A15: (F . g1) = (F1 . g) & (F . f1) = (F1 . f) by Def21;

        

         A16: [(F1 . g), (F1 . f)] in ( dom the Comp of D) by A15, Def2, A13, A1;

        

        thus (F1 . (g (*) f)) = (F1 . (the Comp of C . (g,f))) by A11, CAT_1: 16

        .= (F . (g1 (*) f1)) by A14, Def21

        .= ((F . g1) (*) (F . f1)) by A13, A1

        .= (the Comp of D . ((F1 . g),(F1 . f))) by A15, Def3, A13, A1

        .= ((F1 . g) (*) (F1 . f)) by A16, CAT_1:def 1;

      end;

      hence thesis by A2, A4, CAT_1: 61;

    end;

    theorem :: CAT_6:49

    

     Th50: for C1,C2 be Category st ( alter C1) ~= ( alter C2) holds C1 ~= C2

    proof

      let C1,C2 be Category;

      assume ( alter C1) ~= ( alter C2);

      then

      consider F be Functor of ( alter C1), ( alter C2), G be Functor of ( alter C2), ( alter C1) such that

       A1: F is covariant & G is covariant & (G (*) F) = ( id ( alter C1)) & (F (*) G) = ( id ( alter C2));

      reconsider F1 = F as Functor of C1, C2 by A1, Th49;

      

       A2: ( dom F) = the carrier of ( alter C1) by FUNCT_2:def 1;

      (G (*) F) = (F * G) by A1, Def27;

      then (F * G) = ( id the carrier of ( alter C1)) by A1, STRUCT_0:def 4;

      then

       A3: F is one-to-one by A2, FUNCT_1: 31;

      

       A4: (F (*) G) = (G * F) by A1, Def27;

      

       A5: the carrier' of C2 = ( rng ( id the carrier' of C2))

      .= ( rng (G * F)) by A4, A1, STRUCT_0:def 4;

      the carrier' of C2 c= ( rng F) by A5, RELAT_1: 26;

      then ( rng F1) = the carrier' of C2 by XBOOLE_0:def 10;

      hence C1 ~= C2 by A3, ISOCAT_1:def 4, ISOCAT_1:def 3;

    end;

    theorem :: CAT_6:50

    

     Th51: for C1,C2 be Category st the carrier' of C1 = the carrier' of C2 & the Comp of C1 = the Comp of C2 holds C1 ~= C2

    proof

      let C1,C2 be Category;

      assume the carrier' of C1 = the carrier' of C2 & the Comp of C1 = the Comp of C2;

      then ( alter C1) = ( alter C2);

      hence C1 ~= C2 by Th50;

    end;

    theorem :: CAT_6:51

    for C be Category holds C ~= ( Alter ( alter C)) by Th51;

    theorem :: CAT_6:52

    for C be non empty category holds C ~= ( alter ( Alter C))

    proof

      let C be non empty category;

      set D = ( alter ( Alter C));

      reconsider X = the carrier of C as set;

      reconsider I0 = ( id C) as Function of X, X;

      

       A1: I0 = ( id X) by STRUCT_0:def 4;

      reconsider F = ( id C) as Functor of C, D;

      reconsider G = ( id C) as Functor of D, C;

      for f be morphism of C st f is identity holds (F . f) is identity

      proof

        let f be morphism of C;

        assume

         A2: f is identity;

        (F . f) = (I0 . f) by Def21

        .= (( id X) . f) by STRUCT_0:def 4

        .= f;

        hence (F . f) is identity by A2, Th16, Th18;

      end;

      then

       A3: F is identity-preserving;

      for f1,f2 be morphism of C st f1 |> f2 holds (F . f1) |> (F . f2) & (F . (f1 (*) f2)) = ((F . f1) (*) (F . f2))

      proof

        let f1,f2 be morphism of C;

        assume

         A4: f1 |> f2;

        

         A5: (F . f1) = (I0 . f1) by Def21

        .= (( id X) . f1) by STRUCT_0:def 4

        .= f1;

        

         A6: (F . f2) = (I0 . f2) by Def21

        .= (( id X) . f2) by STRUCT_0:def 4

        .= f2;

        hence

         A7: (F . f1) |> (F . f2) by A4, A5;

        

        thus (F . (f1 (*) f2)) = (I0 . (f1 (*) f2)) by Def21

        .= (( id X) . (f1 (*) f2)) by STRUCT_0:def 4

        .= (the composition of C . (f1,f2)) by A4, Def3

        .= ((F . f1) (*) (F . f2)) by A5, A6, A7, Def3;

      end;

      then F is multiplicative;

      then

       A8: F is covariant by A3;

      for f be morphism of D st f is identity holds (G . f) is identity

      proof

        let f be morphism of D;

        assume

         A9: f is identity;

        (G . f) = (I0 . f) by Def21

        .= (( id X) . f) by STRUCT_0:def 4

        .= f;

        hence (G . f) is identity by A9, Th16, Th18;

      end;

      then

       A10: G is identity-preserving;

      for f1,f2 be morphism of D st f1 |> f2 holds (G . f1) |> (G . f2) & (G . (f1 (*) f2)) = ((G . f1) (*) (G . f2))

      proof

        let f1,f2 be morphism of D;

        assume

         A11: f1 |> f2;

        

         A12: (G . f1) = (I0 . f1) by Def21

        .= (( id X) . f1) by STRUCT_0:def 4

        .= f1;

        

         A13: (G . f2) = (I0 . f2) by Def21

        .= (( id X) . f2) by STRUCT_0:def 4

        .= f2;

        hence

         A14: (G . f1) |> (G . f2) by A11, A12;

        

        thus (G . (f1 (*) f2)) = (I0 . (f1 (*) f2)) by Def21

        .= (( id X) . (f1 (*) f2)) by STRUCT_0:def 4

        .= (the composition of D . (f1,f2)) by A11, Def3

        .= ((G . f1) (*) (G . f2)) by A12, A13, A14, Def3;

      end;

      then G is multiplicative;

      then

       A15: G is covariant by A10;

      

       A16: (G (*) F) = (F * G) by A8, A15, Def27

      .= ( id (X /\ X)) by A1, FUNCT_1: 22

      .= ( id C) by STRUCT_0:def 4;

      (F (*) G) = (G * F) by A8, A15, Def27

      .= ( id (X /\ X)) by A1, FUNCT_1: 22

      .= ( id D) by STRUCT_0:def 4;

      hence C ~= ( alter ( Alter C)) by A8, A15, A16;

    end;