altcat_2.miz

    begin

    reserve e for set;

    theorem :: ALTCAT_2:1

    for X1,X2 be set, a1,a2 be set holds [:(X1 --> a1), (X2 --> a2):] = ( [:X1, X2:] --> [a1, a2])

    proof

      let X1,X2 be set, a1,a2 be set;



       A2: ( dom ( [:X1, X2:] --> [a1, a2])) = [:( dom (X1 --> a1)), ( dom (X2 --> a2)):];

      now

        let x,y be object;

        assume

         A3: x in ( dom (X1 --> a1)) & y in ( dom (X2 --> a2));

        then [x, y] in ( dom ( [:X1, X2:] --> [a1, a2])) by ZFMISC_1: 87;

        then

         A4: [x, y] in [:X1, X2:];

        ((X1 --> a1) . x) = a1 & ((X2 --> a2) . y) = a2 by A3, FUNCOP_1: 7;

        hence (( [:X1, X2:] --> [a1, a2]) . (x,y)) = [((X1 --> a1) . x), ((X2 --> a2) . y)] by A4, FUNCOP_1: 7;

      end;

      hence thesis by A2, FUNCT_3:def 8;

    end;

    registration

      let I be set;

      cluster ( EmptyMS I) -> Function-yielding;

      coherence ;

    end

    theorem :: ALTCAT_2:2

    for f,g be Function holds ( ~ (g * f)) = (g * ( ~ f))

    proof

      let f,g be Function;

       A1:

      now

        let x be object;

        hereby

          assume

           A2: x in ( dom (g * ( ~ f)));

          then x in ( dom ( ~ f)) by FUNCT_1: 11;

          then

          consider y1,z1 be object such that

           A3: x = [z1, y1] and

           A4: [y1, z1] in ( dom f) by FUNCT_4:def 2;

          take y1, z1;

          thus x = [z1, y1] by A3;

          (( ~ f) . (z1,y1)) in ( dom g) by A2, A3, FUNCT_1: 11;

          then (f . (y1,z1)) in ( dom g) by A4, FUNCT_4:def 2;

          hence [y1, z1] in ( dom (g * f)) by A4, FUNCT_1: 11;

        end;

        given y,z be object such that

         A5: x = [z, y] and

         A6: [y, z] in ( dom (g * f));



         A7: [y, z] in ( dom f) by A6, FUNCT_1: 11;

        then

         A8: x in ( dom ( ~ f)) by A5, FUNCT_4:def 2;

        (f . (y,z)) in ( dom g) by A6, FUNCT_1: 11;

        then (( ~ f) . (z,y)) in ( dom g) by A7, FUNCT_4:def 2;

        hence x in ( dom (g * ( ~ f))) by A5, A8, FUNCT_1: 11;

      end;

      now

        let y,z be object;

        assume

         A9: [y, z] in ( dom (g * f));

        then [y, z] in ( dom f) by FUNCT_1: 11;

        then

         A10: [z, y] in ( dom ( ~ f)) by FUNCT_4: 42;



        hence ((g * ( ~ f)) . (z,y)) = (g . (( ~ f) . (z,y))) by FUNCT_1: 13

        .= (g . (f . (y,z))) by A10, FUNCT_4: 43

        .= ((g * f) . (y,z)) by A9, FUNCT_1: 12;

      end;

      hence thesis by A1, FUNCT_4:def 2;

    end;

    theorem :: ALTCAT_2:3

    for f,g,h be Function holds ( ~ (f * [:g, h:])) = (( ~ f) * [:h, g:])

    proof

      let f,g,h be Function;

       A1:

      now

        let x be object;

        hereby

          assume

           A2: x in ( dom (( ~ f) * [:h, g:]));

          then x in ( dom [:h, g:]) by FUNCT_1: 11;

          then x in [:( dom h), ( dom g):] by FUNCT_3:def 8;

          then

          consider y1,z1 be object such that

           A3: y1 in ( dom h) & z1 in ( dom g) and

           A4: x = [y1, z1] by ZFMISC_1: 84;



           A5: ( [:h, g:] . (y1,z1)) = [(h . y1), (g . z1)] & ( [:g, h:] . (z1,y1)) = [(g . z1), (h . y1)] by A3, FUNCT_3:def 8;

          ( [:h, g:] . (y1,z1)) in ( dom ( ~ f)) by A2, A4, FUNCT_1: 11;

          then

           A6: ( [:g, h:] . (z1,y1)) in ( dom f) by A5, FUNCT_4: 42;

          take z1, y1;

          thus x = [y1, z1] by A4;

          ( dom [:g, h:]) = [:( dom g), ( dom h):] by FUNCT_3:def 8;

          then [z1, y1] in ( dom [:g, h:]) by A3, ZFMISC_1: 87;

          hence [z1, y1] in ( dom (f * [:g, h:])) by A6, FUNCT_1: 11;

        end;

        given y,z be object such that

         A7: x = [z, y] and

         A8: [y, z] in ( dom (f * [:g, h:]));



         A9: ( [:g, h:] . (y,z)) in ( dom f) by A8, FUNCT_1: 11;



         A10: ( dom [:g, h:]) = [:( dom g), ( dom h):] by FUNCT_3:def 8;

         [y, z] in ( dom [:g, h:]) by A8, FUNCT_1: 11;

        then

         A11: y in ( dom g) & z in ( dom h) by A10, ZFMISC_1: 87;

        then ( [:g, h:] . (y,z)) = [(g . y), (h . z)] & ( [:h, g:] . (z,y)) = [(h . z), (g . y)] by FUNCT_3:def 8;

        then

         A12: ( [:h, g:] . x) in ( dom ( ~ f)) by A7, A9, FUNCT_4: 42;

        ( dom [:h, g:]) = [:( dom h), ( dom g):] by FUNCT_3:def 8;

        then x in ( dom [:h, g:]) by A7, A11, ZFMISC_1: 87;

        hence x in ( dom (( ~ f) * [:h, g:])) by A12, FUNCT_1: 11;

      end;

      now

        let y,z be object;

        assume

         A13: [y, z] in ( dom (f * [:g, h:]));

        then [y, z] in ( dom [:g, h:]) by FUNCT_1: 11;

        then [y, z] in [:( dom g), ( dom h):] by FUNCT_3:def 8;

        then

         A14: y in ( dom g) & z in ( dom h) by ZFMISC_1: 87;

        ( [:g, h:] . (y,z)) in ( dom f) by A13, FUNCT_1: 11;

        then

         A15: [(g . y), (h . z)] in ( dom f) by A14, FUNCT_3:def 8;

         [z, y] in [:( dom h), ( dom g):] by A14, ZFMISC_1: 87;

        then [z, y] in ( dom [:h, g:]) by FUNCT_3:def 8;



        hence ((( ~ f) * [:h, g:]) . (z,y)) = (( ~ f) . ( [:h, g:] . (z,y))) by FUNCT_1: 13

        .= (( ~ f) . ((h . z),(g . y))) by A14, FUNCT_3:def 8

        .= (f . ((g . y),(h . z))) by A15, FUNCT_4:def 2

        .= (f . ( [:g, h:] . (y,z))) by A14, FUNCT_3:def 8

        .= ((f * [:g, h:]) . (y,z)) by A13, FUNCT_1: 12;

      end;

      hence thesis by A1, FUNCT_4:def 2;

    end;

    registration

      let f be Function-yielding Function;

      cluster ( ~ f) -> Function-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom ( ~ f));

        then

        consider z,y be object such that

         A1: x = [y, z] and

         A2: [z, y] in ( dom f) by FUNCT_4:def 2;

        (f . (z,y)) = (( ~ f) . (y,z)) by A2, FUNCT_4:def 2;

        hence thesis by A1;

      end;

    end

    theorem :: ALTCAT_2:4

    for I be set, A,B,C be ManySortedSet of I st A is_transformable_to B holds for F be ManySortedFunction of A, B, G be ManySortedFunction of B, C holds (G ** F) is ManySortedFunction of A, C

    proof

      let I be set, A,B,C be ManySortedSet of I such that

       A1: A is_transformable_to B;

      let F be ManySortedFunction of A, B, G be ManySortedFunction of B, C;

      reconsider GF = (G ** F) as ManySortedFunction of I by MSSUBFAM: 15;

      GF is ManySortedFunction of A, C

      proof

        let i be object;

        assume

         A2: i in I;

        then

        reconsider Gi = (G . i) as Function of (B . i), (C . i) by PBOOLE:def 15;

        reconsider Fi = (F . i) as Function of (A . i), (B . i) by A2, PBOOLE:def 15;

        i in ( dom GF) by A2, PARTFUN1:def 2;

        then

         A3: ((G ** F) . i) = (Gi * Fi) by PBOOLE:def 19;

        (B . i) = {} implies (A . i) = {} by A1, A2, PZFMISC1:def 3;

        hence thesis by A3, FUNCT_2: 13;

      end;

      hence thesis;

    end;

    registration

      let I be set;

      let A be ManySortedSet of [:I, I:];

      cluster ( ~ A) -> [:I, I:] -defined;

      coherence ;

    end

    registration

      let I be set;

      let A be ManySortedSet of [:I, I:];

      cluster ( ~ A) -> total;

      coherence ;

    end

    theorem :: ALTCAT_2:5

    for I1 be set, I2 be non empty set, f be Function of I1, I2, B,C be ManySortedSet of I2, G be ManySortedFunction of B, C holds (G * f) is ManySortedFunction of (B * f), (C * f)

    proof

      let I1 be set, I2 be non empty set, f be Function of I1, I2, B,C be ManySortedSet of I2, G be ManySortedFunction of B, C;

      let i be object;

      assume

       A1: i in I1;

      then

       A2: (G . (f . i)) is Function of (B . (f . i)), (C . (f . i)) by FUNCT_2: 5, PBOOLE:def 15;



       A3: i in ( dom f) by A1, FUNCT_2:def 1;

      then (B . (f . i)) = ((B * f) . i) & (C . (f . i)) = ((C * f) . i) by FUNCT_1: 13;

      hence thesis by A3, A2, FUNCT_1: 13;

    end;

    definition

      let I be set, A,B be ManySortedSet of [:I, I:], F be ManySortedFunction of A, B;

      :: original: ~

      redefine

      func ~ F -> ManySortedFunction of ( ~ A), ( ~ B) ;

      coherence

      proof

        reconsider G = ( ~ F) as ManySortedSet of [:I, I:];

        G is ManySortedFunction of ( ~ A), ( ~ B)

        proof

          let ii be object;

          assume ii in [:I, I:];

          then

          consider i1,i2 be object such that

           A1: i1 in I & i2 in I and

           A2: ii = [i1, i2] by ZFMISC_1: 84;



           A3: [i2, i1] in [:I, I:] by A1, ZFMISC_1: 87;

          ( dom B) = [:I, I:] by PARTFUN1:def 2;

          then

           A4: (B . (i2,i1)) = (( ~ B) . (i1,i2)) by A3, FUNCT_4:def 2;

          ( dom A) = [:I, I:] by PARTFUN1:def 2;

          then

           A5: (A . (i2,i1)) = (( ~ A) . (i1,i2)) by A3, FUNCT_4:def 2;

          ( dom F) = [:I, I:] by PARTFUN1:def 2;

          then (F . (i2,i1)) = (G . (i1,i2)) by A3, FUNCT_4:def 2;

          hence thesis by A2, A3, A5, A4, PBOOLE:def 15;

        end;

        hence thesis;

      end;

    end

    theorem :: ALTCAT_2:6

    for I1,I2 be non empty set, M be ManySortedSet of [:I1, I2:], o1 be Element of I1, o2 be Element of I2 holds (( ~ M) . (o2,o1)) = (M . (o1,o2))

    proof

      let I1,I2 be non empty set, M be ManySortedSet of [:I1, I2:], o1 be Element of I1, o2 be Element of I2;

       [o1, o2] in [:I1, I2:];

      then [o1, o2] in ( dom M) by PARTFUN1:def 2;

      hence thesis by FUNCT_4:def 2;

    end;

    registration

      let I1 be set, f,g be ManySortedFunction of I1;

      cluster (g ** f) -> I1 -defined;

      coherence

      proof



         A1: ( dom f) = I1 & ( dom g) = I1 by PARTFUN1:def 2;

        ( dom (g ** f)) = (( dom g) /\ ( dom f)) by PBOOLE:def 19

        .= I1 by A1;

        hence thesis;

      end;

    end

    registration

      let I1 be set, f,g be ManySortedFunction of I1;

      cluster (g ** f) -> total;

      coherence

      proof



         A1: ( dom f) = I1 & ( dom g) = I1 by PARTFUN1:def 2;

        ( dom (g ** f)) = (( dom g) /\ ( dom f)) by PBOOLE:def 19

        .= I1 by A1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    begin

    definition

      let f,g be Function;

      :: ALTCAT_2:def1

      pred f cc= g means ( dom f) c= ( dom g) & for i be set st i in ( dom f) holds (f . i) c= (g . i);

      reflexivity ;

    end

    definition

      let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J;

      :: original: cc=

      redefine

      :: ALTCAT_2:def2

      pred A cc= B means I c= J & for i be set st i in I holds (A . i) c= (B . i);

      compatibility

      proof



         A1: ( dom A) = I by PARTFUN1:def 2;

        ( dom B) = J by PARTFUN1:def 2;

        hence A cc= B implies I c= J & for i be set st i in I holds (A . i) c= (B . i) by A1;

        assume that

         A2: I c= J and

         A3: for i be set st i in I holds (A . i) c= (B . i);

        thus ( dom A) c= ( dom B) by A1, A2, PARTFUN1:def 2;

        let i be set;

        assume i in ( dom A);

        hence thesis by A1, A3;

      end;

    end

    theorem :: ALTCAT_2:7



     Th7: for I,J be set, A be ManySortedSet of I, B be ManySortedSet of J holds A cc= B & B cc= A implies A = B

    proof

      let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J;

      assume that

       A1: A cc= B and

       A2: B cc= A;



       A3: I c= J by A1;

      J c= I by A2;

      then I = J by A3, XBOOLE_0:def 10;

      then

      reconsider B9 = B as ManySortedSet of I;

      now

        let i be object;

        assume i in I;

        then (A . i) c= (B . i) & (B . i) c= (A . i) by A1, A2;

        hence (A . i) = (B9 . i) by XBOOLE_0:def 10;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: ALTCAT_2:8



     Th8: for I,J,K be set, A be ManySortedSet of I, B be ManySortedSet of J, C be ManySortedSet of K holds A cc= B & B cc= C implies A cc= C

    proof

      let I,J,K be set, A be ManySortedSet of I, B be ManySortedSet of J, C be ManySortedSet of K;

      assume that

       A1: A cc= B and

       A2: B cc= C;



       A3: I c= J by A1;

      J c= K by A2;

      hence I c= K by A3;

      let i be set;

      assume

       A4: i in I;

      then

       A5: (A . i) c= (B . i) by A1;

      (B . i) c= (C . i) by A2, A3, A4;

      hence thesis by A5;

    end;

    theorem :: ALTCAT_2:9

    for I be set, A be ManySortedSet of I, B be ManySortedSet of I holds A cc= B iff A c= B;

    begin

    scheme :: ALTCAT_2:sch1

    OnSingletons { X() -> non empty set , F( set) -> set , P[ set] } :

{ [o, F(o)] where o be Element of X() : P[o] } is Function;

      set f = { [o, F(o)] where o be Element of X() : P[o] };



       A1: f is Function-like

      proof

        let x,y1,y2 be object;

        assume [x, y1] in f;

        then

        consider o1 be Element of X() such that

         A2: [x, y1] = [o1, F(o1)] and P[o1];



         A3: o1 = x by A2, XTUPLE_0: 1;

        assume [x, y2] in f;

        then

        consider o2 be Element of X() such that

         A4: [x, y2] = [o2, F(o2)] and P[o2];

        o2 = x by A4, XTUPLE_0: 1;

        hence thesis by A2, A4, A3, XTUPLE_0: 1;

      end;

      f is Relation-like

      proof

        let x be object;

        assume x in f;

        then

        consider o be Element of X() such that

         A5: x = [o, F(o)] and P[o];

        take o, F(o);

        thus thesis by A5;

      end;

      hence thesis by A1;

    end;

    scheme :: ALTCAT_2:sch2

    DomOnSingletons { X() -> non empty set , f() -> Function , F( set) -> set , P[ set] } :

( dom f()) = { o where o be Element of X() : P[o] }

      provided

       A1: f() = { [o, F(o)] where o be Element of X() : P[o] };

      set A = { o where o be Element of X() : P[o] };

      now

        let x be object;

        hereby

          assume x in A;

          then

          consider o be Element of X() such that

           A2: x = o & P[o];

          reconsider y = F(o) as object;

          take y;

          thus [x, y] in f() by A1, A2;

        end;

        given y be object such that

         A3: [x, y] in f();

        consider o be Element of X() such that

         A4: [x, y] = [o, F(o)] and

         A5: P[o] by A1, A3;

        x = o by A4, XTUPLE_0: 1;

        hence x in A by A5;

      end;

      hence thesis by XTUPLE_0:def 12;

    end;

    scheme :: ALTCAT_2:sch3

    ValOnSingletons { X() -> non empty set , f() -> Function , x() -> Element of X() , F( set) -> set , P[ set] } :

(f() . x()) = F(x)

      provided

       A1: f() = { [o, F(o)] where o be Element of X() : P[o] }

       and

       A2: P[x()];



       A3: f() = { [o, F(o)] where o be Element of X() : P[o] } by A1;

      ( dom f()) = { o where o be Element of X() : P[o] } from DomOnSingletons( A3);

      then

       A4: x() in ( dom f()) by A2;

       [x(), F(x)] in { [o, F(o)] where o be Element of X() : P[o] } by A2;

      hence thesis by A1, A4, FUNCT_1:def 2;

    end;

    begin

    theorem :: ALTCAT_2:10



     Th10: for C be Category, i,j,k be Object of C holds [:( Hom (j,k)), ( Hom (i,j)):] c= ( dom the Comp of C)

    proof

      let C be Category, i,j,k be Object of C;

      let e be object;

      assume

       A1: e in [:( Hom (j,k)), ( Hom (i,j)):];

      then

      reconsider y = (e `1 ), x = (e `2 ) as Morphism of C by MCART_1: 10;



       A2: (e `2 ) in ( Hom (i,j)) by A1, MCART_1: 10;



       A3: e = [y, x] by A1, MCART_1: 21;

      (e `1 ) in ( Hom (j,k)) by A1, MCART_1: 10;



      then ( dom y) = j by CAT_1: 1

      .= ( cod x) by A2, CAT_1: 1;

      hence thesis by A3, CAT_1: 15;

    end;

    theorem :: ALTCAT_2:11



     Th11: for C be Category, i,j,k be Object of C holds (the Comp of C .: [:( Hom (j,k)), ( Hom (i,j)):]) c= ( Hom (i,k))

    proof

      let C be Category, i,j,k be Object of C;

      let e be object;

      assume e in (the Comp of C .: [:( Hom (j,k)), ( Hom (i,j)):]);

      then

      consider x be object such that

       A1: x in ( dom the Comp of C) and

       A2: x in [:( Hom (j,k)), ( Hom (i,j)):] and

       A3: e = (the Comp of C . x) by FUNCT_1:def 6;

      reconsider y = (x `1 ), z = (x `2 ) as Morphism of C by A2, MCART_1: 10;



       A4: x = [y, z] & e = (the Comp of C . (y,z)) by A2, A3, MCART_1: 21;



       A5: (x `2 ) in ( Hom (i,j)) by A2, MCART_1: 10;

      then

       A6: z is Morphism of i, j by CAT_1:def 5;



       A7: (x `1 ) in ( Hom (j,k)) by A2, MCART_1: 10;

      then y is Morphism of j, k by CAT_1:def 5;

      then (y (*) z) in ( Hom (i,k)) by A7, A5, A6, CAT_1: 23;

      hence thesis by A1, A4, CAT_1:def 1;

    end;

    definition

      let C be non void non empty CatStr;

      :: ALTCAT_2:def3

      func the_hom_sets_of C -> ManySortedSet of [:the carrier of C, the carrier of C:] means

      : Def3: for i,j be Object of C holds (it . (i,j)) = ( Hom (i,j));

      existence

      proof

        deffunc H( Object of C, Object of C) = ( Hom ($1,$2));

        thus ex M be ManySortedSet of [:the carrier of C, the carrier of C:] st for i,j be Object of C holds (M . (i,j)) = H(i,j) from ALTCAT_1:sch 2;

      end;

      uniqueness

      proof

        let M1,M2 be ManySortedSet of [:the carrier of C, the carrier of C:] such that

         A1: for i,j be Object of C holds (M1 . (i,j)) = ( Hom (i,j)) and

         A2: for i,j be Object of C holds (M2 . (i,j)) = ( Hom (i,j));

        now

          let i,j be Object of C;



          thus (M1 . (i,j)) = ( Hom (i,j)) by A1

          .= (M2 . (i,j)) by A2;

        end;

        hence thesis by ALTCAT_1: 7;

      end;

    end

    theorem :: ALTCAT_2:12



     Th12: for C be Category, i be Object of C holds ( id i) in (( the_hom_sets_of C) . (i,i))

    proof

      let C be Category, i be Object of C;

      ( id i) in ( Hom (i,i)) by CAT_1: 27;

      hence thesis by Def3;

    end;

    definition

      let C be Category;

      :: ALTCAT_2:def4

      func the_comps_of C -> BinComp of ( the_hom_sets_of C) means

      : Def4: for i,j,k be Object of C holds (it . (i,j,k)) = (the Comp of C | [:(( the_hom_sets_of C) . (j,k)), (( the_hom_sets_of C) . (i,j)):] qua set);

      existence

      proof

        deffunc F( object) = (the Comp of C | [:(( the_hom_sets_of C) . ((($1 `1 ) `2 ),($1 `2 ))), (( the_hom_sets_of C) . ((($1 `1 ) `1 ),(($1 `1 ) `2 ))):] qua set);

        set Ob3 = [:the carrier of C, the carrier of C, the carrier of C:], G = ( the_hom_sets_of C);

        consider o be Function such that

         A1: ( dom o) = Ob3 and

         A2: for e be object st e in Ob3 holds (o . e) = F(e) from FUNCT_1:sch 3;

        reconsider o as ManySortedSet of Ob3 by A1, PARTFUN1:def 2, RELAT_1:def 18;

        now

          let e be object;

          assume e in ( dom o);

          then (o . e) = (the Comp of C | [:(( the_hom_sets_of C) . (((e `1 ) `2 ),(e `2 ))), (( the_hom_sets_of C) . (((e `1 ) `1 ),((e `1 ) `2 ))):] qua set) by A1, A2;

          hence (o . e) is Function;

        end;

        then

        reconsider o as ManySortedFunction of Ob3 by FUNCOP_1:def 6;

        now

          let e be object;

          reconsider f = (o . e) as Function;

          assume

           A3: e in Ob3;

          then

          consider i,j,k be Object of C such that

           A4: e = [i, j, k] by DOMAIN_1: 3;

          reconsider e9 = e as Element of Ob3 by A3;



           A5: (( [i, j, k] qua set `1 ) `2 ) = (e9 `2_3 ) by A4

          .= j by A4, MCART_1:def 6;



           A6: ( [i, j, k] qua set `2 ) = (e9 `3_3 ) by A4

          .= k by A4, MCART_1:def 7;

          (( [i, j, k] qua set `1 ) `1 ) = (e9 `1_3 ) by A4

          .= i by A4, MCART_1:def 5;

          then

           A7: f = (the Comp of C | [:(G . (j,k)), (G . (i,j)):] qua set) by A2, A4, A5, A6;



           A8: (G . (i,j)) = ( Hom (i,j)) & (G . (j,k)) = ( Hom (j,k)) by Def3;



           A9: ( {|G|} . e) = ( {|G|} . (i,j,k)) by A4, MULTOP_1:def 1

          .= (G . (i,k)) by ALTCAT_1:def 3

          .= ( Hom (i,k)) by Def3;



           A10: ( {|G, G|} . e) = ( {|G, G|} . (i,j,k)) by A4, MULTOP_1:def 1

          .= [:( Hom (j,k)), ( Hom (i,j)):] by A8, ALTCAT_1:def 4;

          (the Comp of C .: [:( Hom (j,k)), ( Hom (i,j)):]) c= ( Hom (i,k)) by Th11;

          then

           A11: ( rng f) c= ( {|G|} . e) by A8, A7, A9, RELAT_1: 115;

           [:( Hom (j,k)), ( Hom (i,j)):] c= ( dom the Comp of C) by Th10;

          then ( dom f) = ( {|G, G|} . e) by A8, A7, A10, RELAT_1: 62;

          hence (o . e) is Function of ( {|G, G|} . e), ( {|G|} . e) by A11, FUNCT_2: 2;

        end;

        then

        reconsider o as BinComp of G by PBOOLE:def 15;

        take o;

        let i,j,k be Object of C;

        reconsider e = [i, j, k] as Element of Ob3;



         A12: (( [i, j, k] qua set `1 ) `1 ) = (e `1_3 )

        .= i by MCART_1:def 5;



         A13: (( [i, j, k] qua set `1 ) `2 ) = (e `2_3 )

        .= j by MCART_1:def 6;



         A14: ( [i, j, k] qua set `2 ) = (e `3_3 )

        .= k by MCART_1:def 7;



        thus (o . (i,j,k)) = (o . [i, j, k]) by MULTOP_1:def 1

        .= (the Comp of C | [:(( the_hom_sets_of C) . (j,k)), (( the_hom_sets_of C) . (i,j)):] qua set) by A2, A12, A13, A14;

      end;

      uniqueness

      proof

        let o1,o2 be BinComp of ( the_hom_sets_of C) such that

         A15: for i,j,k be Object of C holds (o1 . (i,j,k)) = (the Comp of C | [:(( the_hom_sets_of C) . (j,k)), (( the_hom_sets_of C) . (i,j)):] qua set) and

         A16: for i,j,k be Object of C holds (o2 . (i,j,k)) = (the Comp of C | [:(( the_hom_sets_of C) . (j,k)), (( the_hom_sets_of C) . (i,j)):] qua set);

        now

          let a be object;

          assume a in [:the carrier of C, the carrier of C, the carrier of C:];

          then

          consider i,j,k be Object of C such that

           A17: a = [i, j, k] by DOMAIN_1: 3;



          thus (o1 . a) = (o1 . (i,j,k)) by A17, MULTOP_1:def 1

          .= (the Comp of C | [:(( the_hom_sets_of C) . (j,k)), (( the_hom_sets_of C) . (i,j)):] qua set) by A15

          .= (o2 . (i,j,k)) by A16

          .= (o2 . a) by A17, MULTOP_1:def 1;

        end;

        hence o1 = o2;

      end;

    end

    theorem :: ALTCAT_2:13



     Th13: for C be Category, i,j,k be Object of C st ( Hom (i,j)) <> {} & ( Hom (j,k)) <> {} holds for f be Morphism of i, j, g be Morphism of j, k holds ((( the_comps_of C) . (i,j,k)) . (g,f)) = (g * f)

    proof

      let C be Category, i,j,k be Object of C such that

       A1: ( Hom (i,j)) <> {} and

       A2: ( Hom (j,k)) <> {} ;

      let f be Morphism of i, j, g be Morphism of j, k;



       A3: g in ( Hom (j,k)) by A2, CAT_1:def 5;

      then

       A4: g in (( the_hom_sets_of C) . (j,k)) by Def3;



       A5: f in ( Hom (i,j)) by A1, CAT_1:def 5;

      then f in (( the_hom_sets_of C) . (i,j)) by Def3;

      then

       A6: [g, f] in [:(( the_hom_sets_of C) . (j,k)), (( the_hom_sets_of C) . (i,j)):] by A4, ZFMISC_1: 87;



       A7: ( dom g) = j by A3, CAT_1: 1

      .= ( cod f) by A5, CAT_1: 1;



      thus ((( the_comps_of C) . (i,j,k)) . (g,f)) = ((the Comp of C | [:(( the_hom_sets_of C) . (j,k)), (( the_hom_sets_of C) . (i,j)):] qua set) . [g, f]) by Def4

      .= (the Comp of C . (g,f)) by A6, FUNCT_1: 49

      .= (g (*) f qua Morphism of C) by A7, CAT_1: 16

      .= (g * f) by A1, A2, CAT_1:def 13;

    end;

    theorem :: ALTCAT_2:14



     Th14: for C be Category holds ( the_comps_of C) is associative

    proof

      let C be Category;

      let i,j,k,l be Object of C;

      let f,g,h be set;

      assume f in (( the_hom_sets_of C) . (i,j));

      then

       A1: f in ( Hom (i,j)) by Def3;

      then

      reconsider f9 = f as Morphism of i, j by CAT_1:def 5;

      assume g in (( the_hom_sets_of C) . (j,k));

      then

       A2: g in ( Hom (j,k)) by Def3;

      then

      reconsider g9 = g as Morphism of j, k by CAT_1:def 5;

      assume h in (( the_hom_sets_of C) . (k,l));

      then

       A3: h in ( Hom (k,l)) by Def3;

      then

      reconsider h9 = h as Morphism of k, l by CAT_1:def 5;



       A4: ( Hom (j,l)) <> {} & ((( the_comps_of C) . (j,k,l)) . (h,g)) = (h9 * g9) by A2, A3, Th13, CAT_1: 24;

      ( Hom (i,k)) <> {} & ((( the_comps_of C) . (i,j,k)) . (g,f)) = (g9 * f9) by A1, A2, Th13, CAT_1: 24;



      hence ((( the_comps_of C) . (i,k,l)) . (h,((( the_comps_of C) . (i,j,k)) . (g,f)))) = (h9 * (g9 * f9)) by A3, Th13

      .= ((h9 * g9) * f9) by A1, A2, A3, CAT_1: 25

      .= ((( the_comps_of C) . (i,j,l)) . (((( the_comps_of C) . (j,k,l)) . (h,g)),f)) by A1, A4, Th13;

    end;

    theorem :: ALTCAT_2:15



     Th15: for C be Category holds ( the_comps_of C) is with_left_units with_right_units

    proof

      let C be Category;

      thus ( the_comps_of C) is with_left_units

      proof

        let i be Object of C;

        take ( id i);

        thus ( id i) in (( the_hom_sets_of C) . (i,i)) by Th12;

        let j be Object of C, f be set;

        assume f in (( the_hom_sets_of C) . (j,i));

        then

         A1: f in ( Hom (j,i)) by Def3;

        then

        reconsider m = f as Morphism of j, i by CAT_1:def 5;

        ( Hom (i,i)) <> {} ;



        hence ((( the_comps_of C) . (j,i,i)) . (( id i),f)) = (( id i) * m) by A1, Th13

        .= f by A1, CAT_1: 28;

      end;

      let j be Object of C;

      take ( id j);

      thus ( id j) in (( the_hom_sets_of C) . (j,j)) by Th12;

      let i be Object of C, f be set;

      assume f in (( the_hom_sets_of C) . (j,i));

      then

       A2: f in ( Hom (j,i)) by Def3;

      then

      reconsider m = f as Morphism of j, i by CAT_1:def 5;

      ( Hom (j,j)) <> {} ;



      hence ((( the_comps_of C) . (j,j,i)) . (f,( id j))) = (m * ( id j)) by A2, Th13

      .= f by A2, CAT_1: 29;

    end;

    begin

    definition

      let C be Category;

      :: ALTCAT_2:def5

      func Alter C -> strict non empty AltCatStr equals AltCatStr (# the carrier of C, ( the_hom_sets_of C), ( the_comps_of C) #);

      correctness ;

    end

    theorem :: ALTCAT_2:16



     Th16: for C be Category holds ( Alter C) is associative

    proof

      let C be Category;

      thus the Comp of ( Alter C) is associative by Th14;

    end;

    theorem :: ALTCAT_2:17



     Th17: for C be Category holds ( Alter C) is with_units

    proof

      let C be Category;

      thus the Comp of ( Alter C) is with_left_units with_right_units by Th15;

    end;

    theorem :: ALTCAT_2:18



     Th18: for C be Category holds ( Alter C) is transitive

    proof

      let C be Category;

      let o1,o2,o3 be Object of ( Alter C) such that

       A1: <^o1, o2^> <> {} & <^o2, o3^> <> {} ;

      reconsider x1 = o1, x2 = o2, x3 = o3 as Object of C;



       A2: <^o1, o3^> = ( Hom (x1,x3)) by Def3;

       <^o1, o2^> = ( Hom (x1,x2)) & <^o2, o3^> = ( Hom (x2,x3)) by Def3;

      hence thesis by A1, A2, CAT_1: 24;

    end;

    registration

      let C be Category;

      cluster ( Alter C) -> transitive associative with_units;

      coherence by Th16, Th17, Th18;

    end

    begin

    registration

      cluster non empty strict for AltGraph;

      existence

      proof

        set M = the ManySortedSet of [: { {} }, { {} }:];

        take A = AltGraph (# { {} }, M #);

        thus the carrier of A is non empty;

        thus thesis;

      end;

    end

    definition

      let C be AltGraph;

      :: ALTCAT_2:def6

      attr C is reflexive means for x be set st x in the carrier of C holds (the Arrows of C . (x,x)) <> {} ;

    end

    definition

      let C be non empty AltGraph;

      :: original: reflexive

      redefine

      :: ALTCAT_2:def7

      attr C is reflexive means for o be Object of C holds <^o, o^> <> {} ;

      compatibility

      proof

        thus C is reflexive implies for o be Object of C holds <^o, o^> <> {} ;

        assume

         A1: for o be Object of C holds <^o, o^> <> {} ;

        let x be set;

        assume x in the carrier of C;

        then

        reconsider o = x as Object of C;

        (the Arrows of C . (x,x)) = <^o, o^>;

        hence thesis by A1;

      end;

    end

    definition

      let C be non empty transitive AltCatStr;

      :: original: associative

      redefine

      :: ALTCAT_2:def8

      attr C is associative means

      : Def8: for o1,o2,o3,o4 be Object of C holds for f be Morphism of o1, o2, g be Morphism of o2, o3, h be Morphism of o3, o4 st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o4^> <> {} holds ((h * g) * f) = (h * (g * f));

      compatibility

      proof

        thus C is associative implies for o1,o2,o3,o4 be Object of C holds for f be Morphism of o1, o2, g be Morphism of o2, o3, h be Morphism of o3, o4 st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o4^> <> {} holds ((h * g) * f) = (h * (g * f)) by ALTCAT_1: 21;

        assume

         A1: for o1,o2,o3,o4 be Object of C holds for f be Morphism of o1, o2, g be Morphism of o2, o3, h be Morphism of o3, o4 st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o4^> <> {} holds ((h * g) * f) = (h * (g * f));

        let i,j,k,l be Element of C;

        reconsider o1 = i, o2 = j, o3 = k, o4 = l as Object of C;

        let f,g,h be set;

        assume

         A2: f in (the Arrows of C . (i,j));

        then

        reconsider ff = f as Morphism of o1, o2;

        assume

         A3: g in (the Arrows of C . (j,k));

        then

         A4: g in <^o2, o3^>;

        f in <^o1, o2^> by A2;

        then

         A5: <^o1, o3^> <> {} by A4, ALTCAT_1:def 2;

        reconsider gg = g as Morphism of o2, o3 by A3;

        assume

         A6: h in (the Arrows of C . (k,l));

        then

        reconsider hh = h as Morphism of o3, o4;



         A7: ((the Comp of C . (j,k,l)) . (h,g)) = (hh * gg) by A3, A6, ALTCAT_1:def 8;

        h in <^o3, o4^> by A6;

        then

         A8: <^o2, o4^> <> {} by A4, ALTCAT_1:def 2;

        ((the Comp of C . (i,j,k)) . (g,f)) = (gg * ff) by A2, A3, ALTCAT_1:def 8;



        hence ((the Comp of C . (i,k,l)) . (h,((the Comp of C . (i,j,k)) . (g,f)))) = (hh * (gg * ff)) by A6, A5, ALTCAT_1:def 8

        .= ((hh * gg) * ff) by A1, A2, A3, A6

        .= ((the Comp of C . (i,j,l)) . (((the Comp of C . (j,k,l)) . (h,g)),f)) by A2, A8, A7, ALTCAT_1:def 8;

      end;

    end

    definition

      let C be non empty AltCatStr;

      :: original: with_units

      redefine

      :: ALTCAT_2:def9

      attr C is with_units means for o be Object of C holds <^o, o^> <> {} & ex i be Morphism of o, o st for o9 be Object of C, m9 be Morphism of o9, o, m99 be Morphism of o, o9 holds ( <^o9, o^> <> {} implies (i * m9) = m9) & ( <^o, o9^> <> {} implies (m99 * i) = m99);

      compatibility

      proof

        hereby

          assume

           A1: C is with_units;

          then

          reconsider C9 = C as with_units non empty AltCatStr;

          let o be Object of C;

          thus <^o, o^> <> {} by A1, ALTCAT_1: 18;

          reconsider p = o as Object of C9;

          reconsider i = ( idm p) as Morphism of o, o;

          take i;

          let o9 be Object of C, m9 be Morphism of o9, o, m99 be Morphism of o, o9;

          thus <^o9, o^> <> {} implies (i * m9) = m9 by ALTCAT_1: 20;

          thus <^o, o9^> <> {} implies (m99 * i) = m99 by ALTCAT_1:def 17;

        end;

        assume

         A2: for o be Object of C holds <^o, o^> <> {} & ex i be Morphism of o, o st for o9 be Object of C, m9 be Morphism of o9, o, m99 be Morphism of o, o9 holds ( <^o9, o^> <> {} implies (i * m9) = m9) & ( <^o, o9^> <> {} implies (m99 * i) = m99);

        hereby

          let j be Element of C;

          reconsider o = j as Object of C;

          consider m be Morphism of o, o such that

           A3: for o9 be Object of C, m9 be Morphism of o9, o, m99 be Morphism of o, o9 holds ( <^o9, o^> <> {} implies (m * m9) = m9) & ( <^o, o9^> <> {} implies (m99 * m) = m99) by A2;

          reconsider e = m as set;

          take e;



           A4: <^o, o^> <> {} by A2;

          hence e in (the Arrows of C . (j,j));

          let i be Element of C, f be set such that

           A5: f in (the Arrows of C . (i,j));

          reconsider o9 = i as Object of C;

          reconsider m9 = f as Morphism of o9, o by A5;



          thus ((the Comp of C . (i,j,j)) . (e,f)) = (m * m9) by A4, A5, ALTCAT_1:def 8

          .= f by A3, A5;

        end;

        let i be Element of C;

        reconsider o = i as Object of C;

        consider m be Morphism of o, o such that

         A6: for o9 be Object of C, m9 be Morphism of o9, o, m99 be Morphism of o, o9 holds ( <^o9, o^> <> {} implies (m * m9) = m9) & ( <^o, o9^> <> {} implies (m99 * m) = m99) by A2;

        take e = m;



         A7: <^o, o^> <> {} by A2;

        hence e in (the Arrows of C . (i,i));

        let j be Element of C, f be set such that

         A8: f in (the Arrows of C . (i,j));

        reconsider o9 = j as Object of C;

        reconsider m9 = f as Morphism of o, o9 by A8;



        thus ((the Comp of C . (i,i,j)) . (f,e)) = (m9 * m) by A7, A8, ALTCAT_1:def 8

        .= f by A6, A8;

      end;

    end

    registration

      cluster with_units -> reflexive for non empty AltCatStr;

      coherence ;

    end

    registration

      cluster non empty reflexive for AltGraph;

      existence

      proof

        set C = the with_units non empty AltCatStr;

        take C;

        thus thesis;

      end;

    end

    registration

      cluster non empty reflexive for AltCatStr;

      existence

      proof

        set C = the category;

        take C;

        thus thesis;

      end;

    end

    begin



     Lm1: for E1,E2 be strict AltCatStr st the carrier of E1 is empty & the carrier of E2 is empty holds E1 = E2

    proof

      let E1,E2 be strict AltCatStr;

      set C1 = the carrier of E1, C2 = the carrier of E2;

      assume that

       A1: C1 is empty and

       A2: C2 is empty;



       A3: [:C2, C2, C2:] = {} by A2, MCART_1: 31;

       [:C1, C1, C1:] = {} by A1, MCART_1: 31;



      then

       A4: the Comp of E1 = {}

      .= the Comp of E2 by A3;



       A5: [:C2, C2:] = {} by A2, ZFMISC_1: 90;

       [:C1, C1:] = {} by A1, ZFMISC_1: 90;



      then the Arrows of E1 = {}

      .= the Arrows of E2 by A5;

      hence thesis by A1, A2, A4;

    end;

    definition

      :: ALTCAT_2:def10

      func the_empty_category -> strict AltCatStr means

      : Def10: the carrier of it is empty;

      existence

      proof

        reconsider a = {} as set;

        set m = the ManySortedSet of [:a, a:];

        set c = the BinComp of m;

        take AltCatStr (# a, m, c #);

        thus thesis;

      end;

      uniqueness by Lm1;

    end

    registration

      cluster the_empty_category -> empty;

      coherence by Def10;

    end

    registration

      cluster empty strict for AltCatStr;

      existence

      proof

        take the_empty_category ;

        thus thesis;

      end;

    end

    theorem :: ALTCAT_2:19

    for E be empty strict AltCatStr holds E = the_empty_category by Lm1;

    begin

    definition

      let C be AltCatStr;

      :: ALTCAT_2:def11

      mode SubCatStr of C -> AltCatStr means

      : Def11: the carrier of it c= the carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the Comp of C;

      existence ;

    end

    reserve C,C1,C2,C3 for AltCatStr;

    theorem :: ALTCAT_2:20



     Th20: C is SubCatStr of C

    proof

      thus the carrier of C c= the carrier of C;

      thus thesis;

    end;

    theorem :: ALTCAT_2:21

    C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3

    proof

      assume the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 & the Comp of C1 cc= the Comp of C2 & the carrier of C2 c= the carrier of C3 & the Arrows of C2 cc= the Arrows of C3 & the Comp of C2 cc= the Comp of C3;

      hence the carrier of C1 c= the carrier of C3 & the Arrows of C1 cc= the Arrows of C3 & the Comp of C1 cc= the Comp of C3 by Th8;

    end;

    theorem :: ALTCAT_2:22



     Th22: for C1,C2 be AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C1 holds the AltCatStr of C1 = the AltCatStr of C2

    proof

      let C1,C2 be AltCatStr;

      assume that

       A1: the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 and

       A2: the Comp of C1 cc= the Comp of C2 and

       A3: the carrier of C2 c= the carrier of C1 & the Arrows of C2 cc= the Arrows of C1 and

       A4: the Comp of C2 cc= the Comp of C1;

      the carrier of C1 = the carrier of C2 & the Arrows of C1 = the Arrows of C2 by A1, A3, Th7, XBOOLE_0:def 10;

      hence thesis by A2, A4, Th7;

    end;

    registration

      let C be AltCatStr;

      cluster strict for SubCatStr of C;

      existence

      proof

        set D = the AltCatStr of C;

        reconsider D as SubCatStr of C by Def11;

        take D;

        thus thesis;

      end;

    end

    definition

      let C be non empty AltCatStr, o be Object of C;

      :: ALTCAT_2:def12

      func ObCat o -> strict SubCatStr of C means

      : Def12: the carrier of it = {o} & the Arrows of it = ((o,o) :-> <^o, o^>) & the Comp of it = ( [o, o, o] .--> (the Comp of C . (o,o,o)));

      existence

      proof

        set m = ( [o, o, o] .--> (the Comp of C . (o,o,o)));

        ( dom m) = { [o, o, o]}

        .= [: {o}, {o}, {o}:] by MCART_1: 35;

        then

        reconsider m as ManySortedSet of [: {o}, {o}, {o}:];

        set a = ((o,o) :-> <^o, o^>);

        ( dom a) = [: {o}, {o}:] by FUNCT_2:def 1;

        then

        reconsider a as ManySortedSet of [: {o}, {o}:];



         A1: (a . (o,o)) = (the Arrows of C . (o,o)) by FUNCT_4: 80;

        m is ManySortedFunction of {|a, a|}, {|a|}

        proof

          let i be object;



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

          assume i in [: {o}, {o}, {o}:];

          then i in { [o, o, o]} by MCART_1: 35;

          then

           A3: i = [o, o, o] by TARSKI:def 1;



          then

           A4: ( {|a|} . i) = ( {|a|} . (o,o,o)) by MULTOP_1:def 1

          .= (the Arrows of C . (o,o)) by A1, A2, ALTCAT_1:def 3;

          ( {|a, a|} . i) = ( {|a, a|} . (o,o,o)) by A3, MULTOP_1:def 1

          .= [:(the Arrows of C . (o,o)), (the Arrows of C . (o,o)):] by A1, A2, ALTCAT_1:def 4;

          hence thesis by A3, A4, FUNCOP_1: 72;

        end;

        then

        reconsider m as BinComp of a;

        set D = AltCatStr (# {o}, a, m #);

        D is SubCatStr of C

        proof

          thus the carrier of D c= the carrier of C;

          thus the Arrows of D cc= the Arrows of C

          proof

            thus [:the carrier of D, the carrier of D:] c= [:the carrier of C, the carrier of C:];

            let i be set;

            assume i in [:the carrier of D, the carrier of D:];

            then i in { [o, o]} by ZFMISC_1: 29;

            then i = [o, o] by TARSKI:def 1;

            hence thesis by A1;

          end;

          thus [:the carrier of D, the carrier of D, the carrier of D:] c= [:the carrier of C, the carrier of C, the carrier of C:];

          let i be set;

          assume i in [:the carrier of D, the carrier of D, the carrier of D:];

          then i in { [o, o, o]} by MCART_1: 35;

          then

           A5: i = [o, o, o] by TARSKI:def 1;



          then (the Comp of D . i) = (the Comp of C . (o,o,o)) by FUNCOP_1: 72

          .= (the Comp of C . i) by A5, MULTOP_1:def 1;

          hence thesis;

        end;

        then

        reconsider D as strict SubCatStr of C;

        take D;

        thus thesis;

      end;

      uniqueness ;

    end

    reserve C for non empty AltCatStr,

o for Object of C;

    theorem :: ALTCAT_2:23



     Th23: for o9 be Object of ( ObCat o) holds o9 = o

    proof

      let o9 be Object of ( ObCat o);

      the carrier of ( ObCat o) = {o} by Def12;

      hence thesis by TARSKI:def 1;

    end;

    registration

      let C be non empty AltCatStr, o be Object of C;

      cluster ( ObCat o) -> transitive non empty;

      coherence

      proof

        thus ( ObCat o) is transitive

        proof

          let o1,o2,o3 be Object of ( ObCat o);

          assume that <^o1, o2^> <> {} and

           A1: <^o2, o3^> <> {} ;

          o1 = o by Th23;

          hence thesis by A1, Th23;

        end;

        the carrier of ( ObCat o) = {o} by Def12;

        hence the carrier of ( ObCat o) is non empty;

      end;

    end

    registration

      let C be non empty AltCatStr;

      cluster transitive non empty strict for SubCatStr of C;

      existence

      proof

        set o = the Object of C;

        take ( ObCat o);

        thus thesis;

      end;

    end

    theorem :: ALTCAT_2:24



     Th24: for C be transitive non empty AltCatStr, D1,D2 be transitive non empty SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds D1 is SubCatStr of D2

    proof

      let C be transitive non empty AltCatStr, D1,D2 be transitive non empty SubCatStr of C such that

       A1: the carrier of D1 c= the carrier of D2 and

       A2: the Arrows of D1 cc= the Arrows of D2;

      thus the carrier of D1 c= the carrier of D2 by A1;

      thus the Arrows of D1 cc= the Arrows of D2 by A2;

      thus [:the carrier of D1, the carrier of D1, the carrier of D1:] c= [:the carrier of D2, the carrier of D2, the carrier of D2:] by A1, MCART_1: 73;

      let x be set;

      assume

       A3: x in [:the carrier of D1, the carrier of D1, the carrier of D1:];

      then

      consider i1,i2,i3 be object such that

       A4: i1 in the carrier of D1 & i2 in the carrier of D1 & i3 in the carrier of D1 and

       A5: x = [i1, i2, i3] by MCART_1: 68;

      reconsider i1, i2, i3 as Object of D1 by A4;

      reconsider j1 = i1, j2 = i2, j3 = i3 as Object of D2 by A1;

       [i2, i3] in [:the carrier of D1, the carrier of D1:];

      then

       A6: <^i2, i3^> c= <^j2, j3^> by A2;

      reconsider c2 = (the Comp of D2 . (j1,j2,j3)) as Function of [: <^j2, j3^>, <^j1, j2^>:], <^j1, j3^>;

      reconsider c1 = (the Comp of D1 . (i1,i2,i3)) as Function of [: <^i2, i3^>, <^i1, i2^>:], <^i1, i3^>;

       <^i1, i3^> = {} implies <^i2, i3^> = {} or <^i1, i2^> = {} by ALTCAT_1:def 2;

      then <^i1, i3^> = {} implies [: <^i2, i3^>, <^i1, i2^>:] = {} by ZFMISC_1: 90;

      then

       A7: ( dom c1) = [: <^i2, i3^>, <^i1, i2^>:] by FUNCT_2:def 1;

       <^j1, j3^> = {} implies <^j2, j3^> = {} or <^j1, j2^> = {} by ALTCAT_1:def 2;

      then <^j1, j3^> = {} implies [: <^j2, j3^>, <^j1, j2^>:] = {} by ZFMISC_1: 90;

      then

       A8: ( dom c2) = [: <^j2, j3^>, <^j1, j2^>:] by FUNCT_2:def 1;

       [i1, i2] in [:the carrier of D1, the carrier of D1:];

      then <^i1, i2^> c= <^j1, j2^> by A2;

      then

       A9: ( dom c1) c= ( dom c2) by A7, A6, A8, ZFMISC_1: 96;

       A10:

      now

        the carrier of D1 c= the carrier of C by Def11;

        then

        reconsider o1 = i1, o2 = i2, o3 = i3 as Object of C;

        reconsider c = (the Comp of C . (o1,o2,o3)) as Function of [: <^o2, o3^>, <^o1, o2^>:], <^o1, o3^>;

        let y be object;



         A11: c = (the Comp of C . [o1, o2, o3]) by MULTOP_1:def 1;



         A12: c2 = (the Comp of D2 . [o1, o2, o3]) by MULTOP_1:def 1;

         [o1, o2, o3] in [:the carrier of D2, the carrier of D2, the carrier of D2:] & the Comp of D2 cc= the Comp of C by A1, A4, Def11, MCART_1: 69;

        then

         A13: c2 c= c by A11, A12;

        assume

         A14: y in ( dom c1);

        the Comp of D1 cc= the Comp of C & c1 = (the Comp of D1 . [o1, o2, o3]) by Def11, MULTOP_1:def 1;

        then c1 c= c by A3, A5, A11;



        hence (c1 . y) = (c . y) by A14, GRFUNC_1: 2

        .= (c2 . y) by A9, A14, A13, GRFUNC_1: 2;

      end;

      c1 = (the Comp of D1 . x) & c2 = (the Comp of D2 . x) by A5, MULTOP_1:def 1;

      hence thesis by A9, A10, GRFUNC_1: 2;

    end;

    definition

      let C be AltCatStr, D be SubCatStr of C;

      :: ALTCAT_2:def13

      attr D is full means

      : Def13: the Arrows of D = (the Arrows of C || the carrier of D);

    end

    definition

      let C be with_units non empty AltCatStr, D be SubCatStr of C;

      :: ALTCAT_2:def14

      attr D is id-inheriting means

      : Def14: for o be Object of D, o9 be Object of C st o = o9 holds ( idm o9) in <^o, o^> if D is non empty

      otherwise not contradiction;

      consistency ;

    end

    registration

      let C be AltCatStr;

      cluster full strict for SubCatStr of C;

      existence

      proof

        set D = the AltCatStr of C;

        reconsider D as SubCatStr of C by Def11;

        take D;

        thus the Arrows of D = (the Arrows of C || the carrier of D);

        thus thesis;

      end;

    end

    registration

      let C be non empty AltCatStr;

      cluster full non empty strict for SubCatStr of C;

      existence

      proof

        set D = the AltCatStr of C;

        reconsider D as SubCatStr of C by Def11;

        take D;

        thus the Arrows of D = (the Arrows of C || the carrier of D);

        thus the carrier of D is non empty;

        thus thesis;

      end;

    end

    registration

      let C be category, o be Object of C;

      cluster ( ObCat o) -> full id-inheriting;

      coherence

      proof



         A1: the carrier of ( ObCat o) = {o} by Def12;

        the Arrows of ( ObCat o) = ((o,o) :-> <^o, o^>) by Def12

        .= (the Arrows of C || the carrier of ( ObCat o)) by A1, FUNCT_7: 8;

        hence ( ObCat o) is full;

        now

          let o1 be Object of ( ObCat o), o2 be Object of C;

          assume

           A2: o1 = o2;



           A3: o1 = o by Th23;



          then <^o1, o1^> = (((o,o) :-> <^o, o^>) . (o,o)) by Def12

          .= <^o2, o2^> by A3, A2, FUNCT_4: 80;

          hence ( idm o2) in <^o1, o1^> by ALTCAT_1: 19;

        end;

        hence thesis by Def14;

      end;

    end

    registration

      let C be category;

      cluster full id-inheriting non empty strict for SubCatStr of C;

      existence

      proof

        set o = the Object of C;

        take ( ObCat o);

        thus thesis;

      end;

    end

    reserve C for non empty transitive AltCatStr;

    theorem :: ALTCAT_2:25



     Th25: for D be SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds the AltCatStr of D = the AltCatStr of C

    proof

      let D be SubCatStr of C such that

       A1: the carrier of D = the carrier of C and

       A2: the Arrows of D = the Arrows of C;



       A3: D is transitive

      proof

        let o1,o2,o3 be Object of D;

        reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1;

        assume

         A4: <^o1, o2^> <> {} & <^o2, o3^> <> {} ;



         A5: <^o1, o3^> = <^p1, p3^> by A2;

         <^o1, o2^> = <^p1, p2^> & <^o2, o3^> = <^p2, p3^> by A2;

        hence thesis by A5, A4, ALTCAT_1:def 2;

      end;



       A6: C is SubCatStr of C by Th20;

      D is non empty by A1;

      then C is SubCatStr of D by A1, A2, A3, A6, Th24;

      hence thesis by Th22;

    end;

    theorem :: ALTCAT_2:26



     Th26: for D1,D2 be non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds the AltCatStr of D1 = the AltCatStr of D2

    proof

      let D1,D2 be non empty transitive SubCatStr of C;

      assume the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2;

      then D1 is SubCatStr of D2 & D2 is SubCatStr of D1 by Th24;

      hence thesis by Th22;

    end;

    theorem :: ALTCAT_2:27

    for D be full SubCatStr of C st the carrier of D = the carrier of C holds the AltCatStr of D = the AltCatStr of C

    proof

      let D be full SubCatStr of C such that

       A1: the carrier of D = the carrier of C;

      the Arrows of D = (the Arrows of C || the carrier of D) by Def13

      .= the Arrows of C by A1;

      hence thesis by A1, Th25;

    end;

    theorem :: ALTCAT_2:28



     Th28: for C be non empty AltCatStr, D be full non empty SubCatStr of C, o1,o2 be Object of C, p1,p2 be Object of D st o1 = p1 & o2 = p2 holds <^o1, o2^> = <^p1, p2^>

    proof

      let C be non empty AltCatStr, D be full non empty SubCatStr of C, o1,o2 be Object of C, p1,p2 be Object of D such that

       A1: o1 = p1 & o2 = p2;

       [p1, p2] in [:the carrier of D, the carrier of D:];



      hence <^o1, o2^> = ((the Arrows of C || the carrier of D) . (p1,p2)) by A1, FUNCT_1: 49

      .= <^p1, p2^> by Def13;

    end;

    theorem :: ALTCAT_2:29



     Th29: for C be non empty AltCatStr, D be non empty SubCatStr of C holds for o be Object of D holds o is Object of C

    proof

      let C be non empty AltCatStr, D be non empty SubCatStr of C;

      let o be Object of D;

      o in the carrier of D & the carrier of D c= the carrier of C by Def11;

      hence thesis;

    end;

    registration

      let C be transitive non empty AltCatStr;

      cluster full non empty -> transitive for SubCatStr of C;

      coherence

      proof

        let D be SubCatStr of C;

        assume

         A1: D is full non empty;

        let o1,o2,o3 be Object of D such that

         A2: <^o1, o2^> <> {} & <^o2, o3^> <> {} ;

        reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1, Th29;

         <^p1, p2^> <> {} & <^p2, p3^> <> {} by A1, A2, Th28;

        then <^p1, p3^> <> {} by ALTCAT_1:def 2;

        hence thesis by A1, Th28;

      end;

    end

    theorem :: ALTCAT_2:30

    for D1,D2 be full non empty SubCatStr of C st the carrier of D1 = the carrier of D2 holds the AltCatStr of D1 = the AltCatStr of D2

    proof

      let D1,D2 be full non empty SubCatStr of C;

      assume

       A1: the carrier of D1 = the carrier of D2;



      then the Arrows of D1 = (the Arrows of C || the carrier of D2) by Def13

      .= the Arrows of D2 by Def13;

      hence thesis by A1, Th26;

    end;

    theorem :: ALTCAT_2:31



     Th31: for C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be Object of C, p1,p2 be Object of D st o1 = p1 & o2 = p2 holds <^p1, p2^> c= <^o1, o2^>

    proof

      let C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be Object of C, p1,p2 be Object of D such that

       A1: o1 = p1 & o2 = p2;

       [p1, p2] in [:the carrier of D, the carrier of D:] & the Arrows of D cc= the Arrows of C by Def11;

      hence thesis by A1;

    end;

    theorem :: ALTCAT_2:32



     Th32: for C be non empty transitive AltCatStr, D be non empty transitive SubCatStr of C, p1,p2,p3 be Object of D st <^p1, p2^> <> {} & <^p2, p3^> <> {} holds for o1,o2,o3 be Object of C st o1 = p1 & o2 = p2 & o3 = p3 holds for f be Morphism of o1, o2, g be Morphism of o2, o3, ff be Morphism of p1, p2, gg be Morphism of p2, p3 st f = ff & g = gg holds (g * f) = (gg * ff)

    proof

      let C be non empty transitive AltCatStr, D be non empty transitive SubCatStr of C;

      let p1,p2,p3 be Object of D such that

       A1: <^p1, p2^> <> {} & <^p2, p3^> <> {} ;

      let o1,o2,o3 be Object of C such that

       A2: o1 = p1 & o2 = p2 & o3 = p3;

      let f be Morphism of o1, o2, g be Morphism of o2, o3, ff be Morphism of p1, p2, gg be Morphism of p2, p3 such that

       A3: f = ff & g = gg;

       <^p1, p3^> <> {} by A1, ALTCAT_1:def 2;

      then ( dom (the Comp of D . (p1,p2,p3))) = [: <^p2, p3^>, <^p1, p2^>:] by FUNCT_2:def 1;

      then

       A4: [gg, ff] in ( dom (the Comp of D . (p1,p2,p3))) by A1, ZFMISC_1: 87;



       A5: the Comp of D cc= the Comp of C by Def11;

      (the Comp of D . (p1,p2,p3)) = (the Comp of D . [p1, p2, p3]) & (the Comp of C . (o1,o2,o3)) = (the Comp of C . [o1, o2, o3]) by MULTOP_1:def 1;

      then

       A6: (the Comp of D . (p1,p2,p3)) c= (the Comp of C . (o1,o2,o3)) by A2, A5;

       <^o1, o2^> <> {} & <^o2, o3^> <> {} by A1, A2, Th31, XBOOLE_1: 3;



      hence (g * f) = ((the Comp of C . (o1,o2,o3)) . (g,f)) by ALTCAT_1:def 8

      .= ((the Comp of D . (p1,p2,p3)) . (gg,ff)) by A3, A4, A6, GRFUNC_1: 2

      .= (gg * ff) by A1, ALTCAT_1:def 8;

    end;

    registration

      let C be associative transitive non empty AltCatStr;

      cluster transitive -> associative for non empty SubCatStr of C;

      coherence

      proof

        let D be non empty SubCatStr of C;

        assume D is transitive;

        then

        reconsider D as transitive non empty SubCatStr of C;

        D is associative

        proof

          let o1,o2,o3,o4 be Object of D;

          the carrier of D c= the carrier of C by Def11;

          then

          reconsider p1 = o1, p2 = o2, p3 = o3, p4 = o4 as Object of C;

          let f be Morphism of o1, o2, g be Morphism of o2, o3, h be Morphism of o3, o4 such that

           A1: <^o1, o2^> <> {} and

           A2: <^o2, o3^> <> {} and

           A3: <^o3, o4^> <> {} ;



           A4: <^o2, o3^> c= <^p2, p3^> by Th31;

          g in <^o2, o3^> by A2;

          then

          reconsider gg = g as Morphism of p2, p3 by A4;



           A5: <^o1, o2^> c= <^p1, p2^> by Th31;

          f in <^o1, o2^> by A1;

          then

          reconsider ff = f as Morphism of p1, p2 by A5;



           A6: <^o1, o3^> <> {} & (g * f) = (gg * ff) by A1, A2, Th32, ALTCAT_1:def 2;



           A7: <^o3, o4^> c= <^p3, p4^> by Th31;

          h in <^o3, o4^> by A3;

          then

          reconsider hh = h as Morphism of p3, p4 by A7;



           A8: <^p3, p4^> <> {} by A3, Th31, XBOOLE_1: 3;



           A9: <^p1, p2^> <> {} & <^p2, p3^> <> {} by A1, A2, Th31, XBOOLE_1: 3;

           <^o2, o4^> <> {} & (h * g) = (hh * gg) by A2, A3, Th32, ALTCAT_1:def 2;



          hence ((h * g) * f) = ((hh * gg) * ff) by A1, Th32

          .= (hh * (gg * ff)) by A9, A8, Def8

          .= (h * (g * f)) by A3, A6, Th32;

        end;

        hence thesis;

      end;

    end

    theorem :: ALTCAT_2:33



     Th33: for C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be Object of C, p1,p2 be Object of D st o1 = p1 & o2 = p2 & <^p1, p2^> <> {} holds for n be Morphism of p1, p2 holds n is Morphism of o1, o2

    proof

      let C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be Object of C, p1,p2 be Object of D such that

       A1: o1 = p1 & o2 = p2 & <^p1, p2^> <> {} ;

      let n be Morphism of p1, p2;

      n in <^p1, p2^> & <^p1, p2^> c= <^o1, o2^> by A1, Th31;

      hence thesis;

    end;

    registration

      let C be transitive with_units non empty AltCatStr;

      cluster id-inheriting transitive -> with_units for non empty SubCatStr of C;

      coherence

      proof

        let D be non empty SubCatStr of C such that

         A1: D is id-inheriting and

         A2: D is transitive;

        let o be Object of D;

        reconsider p = o as Object of C by Th29;

        reconsider i = ( idm p) as Morphism of o, o by A1, Def14;



         A3: ( idm p) in <^o, o^> by A1, Def14;

        hence <^o, o^> <> {} ;

        take i;

        let o9 be Object of D, m9 be Morphism of o9, o, m99 be Morphism of o, o9;

        hereby

          reconsider p9 = o9 as Object of C by Th29;

          assume

           A4: <^o9, o^> <> {} ;

          then

           A5: <^p9, p^> <> {} by Th31, XBOOLE_1: 3;

          reconsider n9 = m9 as Morphism of p9, p by A4, Th33;



          thus (i * m9) = (( idm p) * n9) by A2, A3, A4, Th32

          .= m9 by A5, ALTCAT_1: 20;

        end;

        reconsider p9 = o9 as Object of C by Th29;

        assume

         A6: <^o, o9^> <> {} ;

        then

         A7: <^p, p9^> <> {} by Th31, XBOOLE_1: 3;

        reconsider n99 = m99 as Morphism of p, p9 by A6, Th33;



        thus (m99 * i) = (n99 * ( idm p)) by A2, A3, A6, Th32

        .= m99 by A7, ALTCAT_1:def 17;

      end;

    end

    registration

      let C be category;

      cluster id-inheriting transitive for non empty SubCatStr of C;

      existence

      proof

        set o = the Object of C;

        take ( ObCat o);

        thus thesis;

      end;

    end

    definition

      let C be category;

      mode subcategory of C is id-inheriting transitive SubCatStr of C;

    end

    theorem :: ALTCAT_2:34

    for C be category, D be non empty subcategory of C holds for o be Object of D, o9 be Object of C st o = o9 holds ( idm o) = ( idm o9)

    proof

      let C be category, D be non empty subcategory of C;

      let o be Object of D, o9 be Object of C;

      assume

       A1: o = o9;

      then

      reconsider m = ( idm o9) as Morphism of o, o by Def14;



       A2: ( idm o9) in <^o, o^> by A1, Def14;

      now

        let p be Object of D such that

         A3: <^o, p^> <> {} ;

        reconsider p9 = p as Object of C by Th29;



         A4: <^o9, p9^> <> {} by A1, A3, Th31, XBOOLE_1: 3;

        let a be Morphism of o, p;

        reconsider n = a as Morphism of o9, p9 by A1, A3, Th33;



        thus (a * m) = (n * ( idm o9)) by A1, A2, A3, Th32

        .= a by A4, ALTCAT_1:def 17;

      end;

      hence thesis by ALTCAT_1:def 17;

    end;