altcat_3.miz



    begin

    definition

      let C be with_units non empty AltCatStr, o1,o2 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o1;

      :: ALTCAT_3:def1

      pred A is_left_inverse_of B means (A * B) = ( idm o2);

    end

    notation

      let C be with_units non empty AltCatStr, o1,o2 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o1;

      synonym B is_right_inverse_of A for A is_left_inverse_of B;

    end

    definition

      let C be with_units non empty AltCatStr, o1,o2 be Object of C, A be Morphism of o1, o2;

      :: ALTCAT_3:def2

      attr A is retraction means ex B be Morphism of o2, o1 st B is_right_inverse_of A;

    end

    definition

      let C be with_units non empty AltCatStr, o1,o2 be Object of C, A be Morphism of o1, o2;

      :: ALTCAT_3:def3

      attr A is coretraction means ex B be Morphism of o2, o1 st B is_left_inverse_of A;

    end

    theorem :: ALTCAT_3:1

    

     Th1: for C be with_units non empty AltCatStr, o be Object of C holds ( idm o) is retraction & ( idm o) is coretraction

    proof

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

       <^o, o^> <> {} by ALTCAT_1: 19;

      then (( idm o) * ( idm o)) = ( idm o) by ALTCAT_1:def 17;

      then ( idm o) is_left_inverse_of ( idm o);

      hence thesis;

    end;

    definition

      let C be category, o1,o2 be Object of C;

      let A be Morphism of o1, o2;

      :: ALTCAT_3:def4

      func A " -> Morphism of o2, o1 means

      : Def4: it is_left_inverse_of A & it is_right_inverse_of A;

      existence

      proof

        consider B1 be Morphism of o2, o1 such that

         A4: B1 is_right_inverse_of A by A3;

        take B1;

        consider B2 be Morphism of o2, o1 such that

         A5: B2 is_left_inverse_of A by A3;

        B1 = (( idm o1) * B1) by A2, ALTCAT_1: 20

        .= ((B2 * A) * B1) by A5

        .= (B2 * (A * B1)) by A1, A2, ALTCAT_1: 21

        .= (B2 * ( idm o2)) by A4

        .= B2 by A2, ALTCAT_1:def 17;

        hence thesis by A4, A5;

      end;

      uniqueness

      proof

        let M1,M2 be Morphism of o2, o1 such that

         A6: M1 is_left_inverse_of A and M1 is_right_inverse_of A and M2 is_left_inverse_of A and

         A7: M2 is_right_inverse_of A;

        

        thus M1 = (M1 * ( idm o2)) by A2, ALTCAT_1:def 17

        .= (M1 * (A * M2)) by A7

        .= ((M1 * A) * M2) by A1, A2, ALTCAT_1: 21

        .= (( idm o1) * M2) by A6

        .= M2 by A2, ALTCAT_1: 20;

      end;

    end

    theorem :: ALTCAT_3:2

    

     Th2: for C be category, o1,o2 be Object of C st <^o1, o2^> <> {} & <^o2, o1^> <> {} holds for A be Morphism of o1, o2 st A is retraction & A is coretraction holds ((A " ) * A) = ( idm o1) & (A * (A " )) = ( idm o2)

    proof

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

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

      let A be Morphism of o1, o2;

      assume A is retraction & A is coretraction;

      then (A " ) is_left_inverse_of A & (A " ) is_right_inverse_of A by A1, Def4;

      hence thesis;

    end;

    theorem :: ALTCAT_3:3

    

     Th3: for C be category, o1,o2 be Object of C st <^o1, o2^> <> {} & <^o2, o1^> <> {} holds for A be Morphism of o1, o2 st A is retraction & A is coretraction holds ((A " ) " ) = A

    proof

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

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

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

      let A be Morphism of o1, o2;

      assume

       A3: A is retraction & A is coretraction;

      then (A " ) is_left_inverse_of A by A1, A2, Def4;

      then

       A4: (A " ) is retraction;

      

       A5: (A " ) is_right_inverse_of A by A1, A2, A3, Def4;

      then (A " ) is coretraction;

      then

       A6: ((A " ) " ) is_right_inverse_of (A " ) by A1, A2, A4, Def4;

      

      thus ((A " ) " ) = (( idm o2) * ((A " ) " )) by A1, ALTCAT_1: 20

      .= ((A * (A " )) * ((A " ) " )) by A5

      .= (A * ((A " ) * ((A " ) " ))) by A1, A2, ALTCAT_1: 21

      .= (A * ( idm o1)) by A6

      .= A by A1, ALTCAT_1:def 17;

    end;

    theorem :: ALTCAT_3:4

    

     Th4: for C be category, o be Object of C holds (( idm o) " ) = ( idm o)

    proof

      let C be category, o be Object of C;

      

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

      ( idm o) is retraction & ( idm o) is coretraction by Th1;

      then

       A2: (( idm o) " ) is_left_inverse_of ( idm o) by A1, Def4;

      

      thus (( idm o) " ) = ((( idm o) " ) * ( idm o)) by A1, ALTCAT_1:def 17

      .= ( idm o) by A2;

    end;

    definition

      let C be category, o1,o2 be Object of C, A be Morphism of o1, o2;

      :: ALTCAT_3:def5

      attr A is iso means (A * (A " )) = ( idm o2) & ((A " ) * A) = ( idm o1);

    end

    theorem :: ALTCAT_3:5

    

     Th5: for C be category, o1,o2 be Object of C, A be Morphism of o1, o2 st A is iso holds A is retraction coretraction

    proof

      let C be category, o1,o2 be Object of C, A be Morphism of o1, o2;

      assume

       A1: A is iso;

      then (A * (A " )) = ( idm o2);

      then (A " ) is_right_inverse_of A;

      hence A is retraction;

      ((A " ) * A) = ( idm o1) by A1;

      then (A " ) is_left_inverse_of A;

      hence thesis;

    end;

    theorem :: ALTCAT_3:6

    

     Th6: for C be category, o1,o2 be Object of C st <^o1, o2^> <> {} & <^o2, o1^> <> {} holds for A be Morphism of o1, o2 holds A is iso iff A is retraction & A is coretraction

    proof

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

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

      let A be Morphism of o1, o2;

      thus A is iso implies A is retraction & A is coretraction by Th5;

      assume

       A2: A is retraction & A is coretraction;

      then (A " ) is_right_inverse_of A by A1, Def4;

      then

       A3: (A * (A " )) = ( idm o2);

      (A " ) is_left_inverse_of A by A1, A2, Def4;

      then ((A " ) * A) = ( idm o1);

      hence thesis by A3;

    end;

    theorem :: ALTCAT_3:7

    

     Th7: for C be category, o1,o2,o3 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o3 st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o1^> <> {} & A is iso & B is iso holds (B * A) is iso & ((B * A) " ) = ((A " ) * (B " ))

    proof

      let C be category, o1,o2,o3 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume that

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

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

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

      assume that

       A4: A is iso and

       A5: B is iso;

      consider A1 be Morphism of o2, o1 such that

       A6: A1 = (A " );

      

       A7: <^o2, o1^> <> {} by A2, A3, ALTCAT_1:def 2;

      then

       A8: A is retraction & A is coretraction by A1, A4, Th6;

      consider B1 be Morphism of o3, o2 such that

       A9: B1 = (B " );

      

       A10: <^o3, o2^> <> {} by A1, A3, ALTCAT_1:def 2;

      then

       A11: B is retraction & B is coretraction by A2, A5, Th6;

      

       A12: ((B * A) * (A1 * B1)) = (B * (A * (A1 * B1))) by A1, A2, A3, ALTCAT_1: 21

      .= (B * ((A * A1) * B1)) by A1, A7, A10, ALTCAT_1: 21

      .= (B * (( idm o2) * B1)) by A1, A7, A8, A6, Th2

      .= (B * B1) by A10, ALTCAT_1: 20

      .= ( idm o3) by A2, A10, A11, A9, Th2;

      then

       A13: (A1 * B1) is_right_inverse_of (B * A);

      then

       A14: (B * A) is retraction;

      

       A15: <^o1, o3^> <> {} by A1, A2, ALTCAT_1:def 2;

      

      then

       A16: ((A1 * B1) * (B * A)) = (A1 * (B1 * (B * A))) by A7, A10, ALTCAT_1: 21

      .= (A1 * ((B1 * B) * A)) by A1, A2, A10, ALTCAT_1: 21

      .= (A1 * (( idm o2) * A)) by A2, A10, A11, A9, Th2

      .= (A1 * A) by A1, ALTCAT_1: 20

      .= ( idm o1) by A1, A7, A8, A6, Th2;

      then

       A17: (A1 * B1) is_left_inverse_of (B * A);

      then (B * A) is coretraction;

      then (A1 * B1) = ((B * A) " ) by A3, A15, A17, A13, A14, Def4;

      hence thesis by A6, A9, A16, A12;

    end;

    definition

      let C be category, o1,o2 be Object of C;

      :: ALTCAT_3:def6

      pred o1,o2 are_iso means <^o1, o2^> <> {} & <^o2, o1^> <> {} & ex A be Morphism of o1, o2 st A is iso;

      reflexivity

      proof

        let o be Object of C;

        thus

         A1: <^o, o^> <> {} & <^o, o^> <> {} by ALTCAT_1: 19;

        take ( idm o);

        set A = ( idm o);

        

         A2: ((A " ) * A) = (A * A) by Th4

        .= ( idm o) by A1, ALTCAT_1:def 17;

        (A * (A " )) = (A * A) by Th4

        .= ( idm o) by A1, ALTCAT_1:def 17;

        hence thesis by A2;

      end;

      symmetry

      proof

        let o1,o2 be Object of C;

        assume that

         A3: <^o1, o2^> <> {} & <^o2, o1^> <> {} and

         A4: ex A be Morphism of o1, o2 st A is iso;

        thus <^o2, o1^> <> {} & <^o1, o2^> <> {} by A3;

        consider A be Morphism of o1, o2 such that

         A5: A is iso by A4;

        take A1 = (A " );

        

         A6: A is retraction & A is coretraction by A5, Th5;

        

        then

         A7: ((A1 " ) * A1) = (A * (A " )) by A3, Th3

        .= ( idm o2) by A3, A6, Th2;

        (A1 * (A1 " )) = ((A " ) * A) by A3, A6, Th3

        .= ( idm o1) by A3, A6, Th2;

        hence thesis by A7;

      end;

    end

    theorem :: ALTCAT_3:8

    for C be category, o1,o2,o3 be Object of C st (o1,o2) are_iso & (o2,o3) are_iso holds (o1,o3) are_iso

    proof

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

       A1: (o1,o2) are_iso and

       A2: (o2,o3) are_iso ;

      

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

      consider B be Morphism of o2, o3 such that

       A4: B is iso by A2;

      consider A be Morphism of o1, o2 such that

       A5: A is iso by A1;

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

      hence

       A6: <^o1, o3^> <> {} & <^o3, o1^> <> {} by A3, ALTCAT_1:def 2;

      take (B * A);

      thus thesis by A3, A6, A5, A4, Th7;

    end;

    definition

      let C be non empty AltCatStr, o1,o2 be Object of C, A be Morphism of o1, o2;

      :: ALTCAT_3:def7

      attr A is mono means for o be Object of C st <^o, o1^> <> {} holds for B,C be Morphism of o, o1 st (A * B) = (A * C) holds B = C;

    end

    definition

      let C be non empty AltCatStr, o1,o2 be Object of C, A be Morphism of o1, o2;

      :: ALTCAT_3:def8

      attr A is epi means for o be Object of C st <^o2, o^> <> {} holds for B,C be Morphism of o2, o st (B * A) = (C * A) holds B = C;

    end

    theorem :: ALTCAT_3:9

    

     Th9: for C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for A be Morphism of o1, o2, B be Morphism of o2, o3 st A is mono & B is mono holds (B * A) is mono

    proof

      let C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C;

      assume that

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

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

      let A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume that

       A3: A is mono and

       A4: B is mono;

      let o be Object of C;

      assume

       A5: <^o, o1^> <> {} ;

      then

       A6: <^o, o2^> <> {} by A1, ALTCAT_1:def 2;

      let M1,M2 be Morphism of o, o1;

      assume

       A7: ((B * A) * M1) = ((B * A) * M2);

      ((B * A) * M1) = (B * (A * M1)) & ((B * A) * M2) = (B * (A * M2)) by A1, A2, A5, ALTCAT_1: 21;

      then (A * M1) = (A * M2) by A4, A7, A6;

      hence thesis by A3, A5;

    end;

    theorem :: ALTCAT_3:10

    

     Th10: for C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for A be Morphism of o1, o2, B be Morphism of o2, o3 st A is epi & B is epi holds (B * A) is epi

    proof

      let C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C;

      assume that

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

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

      let A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume that

       A3: A is epi and

       A4: B is epi;

      let o be Object of C;

      assume

       A5: <^o3, o^> <> {} ;

      then

       A6: <^o2, o^> <> {} by A2, ALTCAT_1:def 2;

      let M1,M2 be Morphism of o3, o;

      assume

       A7: (M1 * (B * A)) = (M2 * (B * A));

      (M1 * (B * A)) = ((M1 * B) * A) & (M2 * (B * A)) = ((M2 * B) * A) by A1, A2, A5, ALTCAT_1: 21;

      then (M1 * B) = (M2 * B) by A3, A7, A6;

      hence thesis by A4, A5;

    end;

    theorem :: ALTCAT_3:11

    for C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for A be Morphism of o1, o2, B be Morphism of o2, o3 st (B * A) is mono holds A is mono

    proof

      let C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C;

      assume

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

      let A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume

       A2: (B * A) is mono;

      let o be Object of C;

      assume

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

      let M1,M2 be Morphism of o, o1;

      assume

       A4: (A * M1) = (A * M2);

      ((B * A) * M1) = (B * (A * M1)) & ((B * A) * M2) = (B * (A * M2)) by A1, A3, ALTCAT_1: 21;

      hence thesis by A2, A3, A4;

    end;

    theorem :: ALTCAT_3:12

    for C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for A be Morphism of o1, o2, B be Morphism of o2, o3 st (B * A) is epi holds B is epi

    proof

      let C be associative transitive non empty AltCatStr, o1,o2,o3 be Object of C;

      assume

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

      let A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume

       A2: (B * A) is epi;

      let o be Object of C;

      assume

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

      let M1,M2 be Morphism of o3, o;

      assume

       A4: (M1 * B) = (M2 * B);

      ((M1 * B) * A) = (M1 * (B * A)) & ((M2 * B) * A) = (M2 * (B * A)) by A1, A3, ALTCAT_1: 21;

      hence thesis by A2, A3, A4;

    end;

     Lm1:

    now

      let C be with_units non empty AltCatStr, a be Object of C;

      thus ( idm a) is epi

      proof

        let o be Object of C such that

         A1: <^a, o^> <> {} ;

        let B,C be Morphism of a, o such that

         A2: (B * ( idm a)) = (C * ( idm a));

        

        thus B = (B * ( idm a)) by A1, ALTCAT_1:def 17

        .= C by A1, A2, ALTCAT_1:def 17;

      end;

      thus ( idm a) is mono

      proof

        let o be Object of C such that

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

        let B,C be Morphism of o, a such that

         A4: (( idm a) * B) = (( idm a) * C);

        

        thus B = (( idm a) * B) by A3, ALTCAT_1: 20

        .= C by A3, A4, ALTCAT_1: 20;

      end;

    end;

    theorem :: ALTCAT_3:13

    for X be non empty set holds for o1,o2 be Object of ( EnsCat X) st <^o1, o2^> <> {} holds for A be Morphism of o1, o2, F be Function of o1, o2 st F = A holds A is mono iff F is one-to-one

    proof

      let X be non empty set, o1,o2 be Object of ( EnsCat X);

      assume

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

      let A be Morphism of o1, o2, F be Function of o1, o2;

      assume

       A2: F = A;

      per cases ;

        suppose o2 <> {} ;

        then

         A3: ( dom F) = o1 by FUNCT_2:def 1;

        thus A is mono implies F is one-to-one

        proof

          set o = o1;

          assume

           A4: A is mono;

          assume not F is one-to-one;

          then

          consider x1,x2 be object such that

           A5: x1 in ( dom F) and

           A6: x2 in ( dom F) and

           A7: (F . x1) = (F . x2) and

           A8: x1 <> x2 by FUNCT_1:def 4;

          set C = (o --> x2);

          set B = (o --> x1);

          

           A9: ( dom C) = o by FUNCOP_1: 13;

          

           A10: ( rng C) c= o1

          proof

            let y be object;

            assume y in ( rng C);

            then ex x be object st x in ( dom C) & (C . x) = y by FUNCT_1:def 3;

            hence thesis by A3, A6, A9, FUNCOP_1: 7;

          end;

          then

           A11: ( dom (F * C)) = o by A3, A9, RELAT_1: 27;

          C in ( Funcs (o,o1)) by A9, A10, FUNCT_2:def 2;

          then

          reconsider C1 = C as Morphism of o, o1 by ALTCAT_1:def 14;

          set o9 = the Element of o;

          

           A12: <^o, o1^> <> {} by ALTCAT_1: 19;

          (B . o9) = x1 by A3, A5, FUNCOP_1: 7;

          then

           A13: (B . o9) <> (C . o9) by A3, A5, A8, FUNCOP_1: 7;

          

           A14: ( dom B) = o by FUNCOP_1: 13;

          

           A15: ( rng B) c= o1

          proof

            let y be object;

            assume y in ( rng B);

            then ex x be object st x in ( dom B) & (B . x) = y by FUNCT_1:def 3;

            hence thesis by A3, A5, A14, FUNCOP_1: 7;

          end;

          then B in ( Funcs (o,o1)) by A14, FUNCT_2:def 2;

          then

          reconsider B1 = B as Morphism of o, o1 by ALTCAT_1:def 14;

          

           A16: ( dom (F * B)) = o by A3, A14, A15, RELAT_1: 27;

          now

            let z be object;

            assume

             A17: z in o;

            

            hence ((F * B) . z) = (F . (B . z)) by A16, FUNCT_1: 12

            .= (F . x2) by A7, A17, FUNCOP_1: 7

            .= (F . (C . z)) by A17, FUNCOP_1: 7

            .= ((F * C) . z) by A11, A17, FUNCT_1: 12;

          end;

          then (F * B) = (F * C) by A16, A11, FUNCT_1: 2;

          

          then (A * B1) = (F * C) by A1, A2, A12, ALTCAT_1: 16

          .= (A * C1) by A1, A2, A12, ALTCAT_1: 16;

          hence contradiction by A4, A12, A13;

        end;

        thus F is one-to-one implies A is mono

        proof

          assume

           A18: F is one-to-one;

          let o be Object of ( EnsCat X);

          assume

           A19: <^o, o1^> <> {} ;

          then

           A20: <^o, o2^> <> {} by A1, ALTCAT_1:def 2;

          let B,C be Morphism of o, o1;

          

           A21: <^o, o1^> = ( Funcs (o,o1)) by ALTCAT_1:def 14;

          then

          consider B1 be Function such that

           A22: B1 = B and

           A23: ( dom B1) = o and

           A24: ( rng B1) c= o1 by A19, FUNCT_2:def 2;

          consider C1 be Function such that

           A25: C1 = C and

           A26: ( dom C1) = o and

           A27: ( rng C1) c= o1 by A19, A21, FUNCT_2:def 2;

          assume (A * B) = (A * C);

          

          then

           A28: (F * B1) = (A * C) by A1, A2, A19, A22, A20, ALTCAT_1: 16

          .= (F * C1) by A1, A2, A19, A25, A20, ALTCAT_1: 16;

          now

            let z be object;

            assume

             A29: z in o;

            then (F . (B1 . z)) = ((F * B1) . z) by A23, FUNCT_1: 13;

            then

             A30: (F . (B1 . z)) = (F . (C1 . z)) by A26, A28, A29, FUNCT_1: 13;

            (B1 . z) in ( rng B1) & (C1 . z) in ( rng C1) by A23, A26, A29, FUNCT_1:def 3;

            hence (B1 . z) = (C1 . z) by A3, A18, A24, A27, A30, FUNCT_1:def 4;

          end;

          hence thesis by A22, A23, A25, A26, FUNCT_1: 2;

        end;

      end;

        suppose

         A31: o2 = {} ;

        then F = {} ;

        hence A is mono implies F is one-to-one;

        thus F is one-to-one implies A is mono

        proof

          set x = the Element of ( Funcs (o1,o2));

          assume F is one-to-one;

          let o be Object of ( EnsCat X);

          assume

           A32: <^o, o1^> <> {} ;

           <^o1, o2^> = ( Funcs (o1,o2)) by ALTCAT_1:def 14;

          then

          consider f be Function such that f = x and

           A33: ( dom f) = o1 and

           A34: ( rng f) c= o2 by A1, FUNCT_2:def 2;

          let B,C be Morphism of o, o1;

          

           A35: <^o, o1^> = ( Funcs (o,o1)) by ALTCAT_1:def 14;

          then

          consider B1 be Function such that

           A36: B1 = B and

           A37: ( dom B1) = o and

           A38: ( rng B1) c= o1 by A32, FUNCT_2:def 2;

          ( rng f) = {} by A31, A34, XBOOLE_1: 3;

          then ( dom f) = {} by RELAT_1: 42;

          then

           A39: ( rng B1) = {} by A38, A33, XBOOLE_1: 3;

          then

           A40: ( dom B1) = {} by RELAT_1: 42;

          assume (A * B) = (A * C);

          consider C1 be Function such that

           A41: C1 = C and

           A42: ( dom C1) = o and ( rng C1) c= o1 by A32, A35, FUNCT_2:def 2;

          B1 = {} by A39, RELAT_1: 41

          .= C1 by A37, A42, A40, RELAT_1: 41;

          hence thesis by A36, A41;

        end;

      end;

    end;

    theorem :: ALTCAT_3:14

    for X be non empty with_non-empty_elements set holds for o1,o2 be Object of ( EnsCat X) st <^o1, o2^> <> {} holds for A be Morphism of o1, o2, F be Function of o1, o2 st F = A holds A is epi iff F is onto

    proof

      let X be non empty with_non-empty_elements set, o1,o2 be Object of ( EnsCat X);

      assume

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

      let A be Morphism of o1, o2, F be Function of o1, o2;

      assume

       A2: F = A;

      per cases ;

        suppose

         A3: for x be set st x in X holds x is trivial;

        thus A is epi implies F is onto

        proof

          assume A is epi;

          now

            per cases ;

              suppose

               A4: o2 = {} ;

              then F = {} ;

              hence thesis by A4, FUNCT_2:def 3, RELAT_1: 38;

            end;

              suppose

               A5: o2 <> {} ;

              

               A6: o1 is Element of X by ALTCAT_1:def 14;

              then o1 is trivial by A3;

              then

              consider z be object such that

               A7: o1 = {z} by A6, ZFMISC_1: 131;

              ( dom F) = {z} by A5, A7, FUNCT_2:def 1;

              then

               A8: ( rng F) <> {} by RELAT_1: 42;

              o2 is Element of X by ALTCAT_1:def 14;

              then o2 is trivial by A3;

              then

              consider y be object such that

               A9: o2 = {y} by A5, ZFMISC_1: 131;

              ( rng F) c= {y} by A9, RELAT_1:def 19;

              then ( rng F) = {y} by A8, ZFMISC_1: 33;

              hence thesis by A9, FUNCT_2:def 3;

            end;

          end;

          hence thesis;

        end;

        thus F is onto implies A is epi

        proof

          assume

           A10: F is onto;

          let o be Object of ( EnsCat X);

          assume

           A11: <^o2, o^> <> {} ;

          then

           A12: <^o1, o^> <> {} by A1, ALTCAT_1:def 2;

          let B,C be Morphism of o2, o;

          

           A13: <^o2, o^> = ( Funcs (o2,o)) by ALTCAT_1:def 14;

          then

          consider B1 be Function such that

           A14: B1 = B and

           A15: ( dom B1) = o2 and ( rng B1) c= o by A11, FUNCT_2:def 2;

          consider C1 be Function such that

           A16: C1 = C and

           A17: ( dom C1) = o2 and ( rng C1) c= o by A11, A13, FUNCT_2:def 2;

          assume (B * A) = (C * A);

          

          then

           A18: (B1 * F) = (C * A) by A1, A2, A11, A14, A12, ALTCAT_1: 16

          .= (C1 * F) by A1, A2, A11, A16, A12, ALTCAT_1: 16;

          now

            assume B1 <> C1;

            then

            consider z be object such that

             A19: z in o2 and

             A20: (B1 . z) <> (C1 . z) by A15, A17, FUNCT_1: 2;

            z in ( rng F) by A10, A19, FUNCT_2:def 3;

            then

            consider x be object such that

             A21: x in ( dom F) and

             A22: (F . x) = z by FUNCT_1:def 3;

            (B1 . (F . x)) = ((B1 * F) . x) by A21, FUNCT_1: 13;

            hence contradiction by A18, A20, A21, A22, FUNCT_1: 13;

          end;

          hence thesis by A14, A16;

        end;

      end;

        suppose

         A23: ex x be set st x in X & x is non trivial;

        now

          per cases ;

            suppose

             A24: o2 <> {} ;

            consider o be set such that

             A25: o in X and

             A26: o is non trivial by A23;

            reconsider o as Object of ( EnsCat X) by A25, ALTCAT_1:def 14;

            

             A27: ( dom F) = o1 by A24, FUNCT_2:def 1;

            thus A is epi implies F is onto

            proof

              set k = the Element of o;

              

               A28: ( rng F) c= o2 by RELAT_1:def 19;

              reconsider ok = (o \ {k}) as non empty set by A26, ZFMISC_1: 139;

              assume that

               A29: A is epi and

               A30: not F is onto;

              ( rng F) <> o2 by A30, FUNCT_2:def 3;

              then not o2 c= ( rng F) by A28, XBOOLE_0:def 10;

              then

              consider y be object such that

               A31: y in o2 and

               A32: not y in ( rng F);

              set C = (o2 --> k);

              

               A33: ( dom C) = o2 by FUNCOP_1: 13;

              

               A34: o <> {} by A25;

              then

               A35: k in o;

              ( rng C) c= o

              proof

                let y be object;

                assume y in ( rng C);

                then ex x be object st x in ( dom C) & (C . x) = y by FUNCT_1:def 3;

                hence thesis by A35, A33, FUNCOP_1: 7;

              end;

              then C in ( Funcs (o2,o)) by A33, FUNCT_2:def 2;

              then

              reconsider C1 = C as Morphism of o2, o by ALTCAT_1:def 14;

              set l = the Element of ok;

              

               A36: not l in {k} by XBOOLE_0:def 5;

              reconsider l as Element of o by XBOOLE_0:def 5;

              

               A37: k <> l by A36, TARSKI:def 1;

              deffunc G( object) = ( IFEQ ($1,y,l,k));

              consider B be Function such that

               A38: ( dom B) = o2 and

               A39: for x be object st x in o2 holds (B . x) = G(x) from FUNCT_1:sch 3;

              

               A40: ( dom (B * F)) = o1 by A27, A28, A38, RELAT_1: 27;

              

               A41: ( rng B) c= o

              proof

                let y1 be object;

                assume y1 in ( rng B);

                then

                consider x be object such that

                 A42: x in ( dom B) & (B . x) = y1 by FUNCT_1:def 3;

                per cases ;

                  suppose

                   A43: x = y;

                  y1 = ( IFEQ (x,y,l,k)) by A38, A39, A42

                  .= l by A43, FUNCOP_1:def 8;

                  hence thesis by A34;

                end;

                  suppose

                   A44: x <> y;

                  y1 = ( IFEQ (x,y,l,k)) by A38, A39, A42

                  .= k by A44, FUNCOP_1:def 8;

                  hence thesis by A34;

                end;

              end;

              then

               A45: B in ( Funcs (o2,o)) by A38, FUNCT_2:def 2;

              then

               A46: B in <^o2, o^> by ALTCAT_1:def 14;

              reconsider B1 = B as Morphism of o2, o by A45, ALTCAT_1:def 14;

              for z be object holds z in ( rng (B * F)) implies z in ( rng B) by FUNCT_1: 14;

              then ( rng (B * F)) c= ( rng B);

              then ( rng (B * F)) c= o by A41;

              then (B * F) in ( Funcs (o1,o)) by A40, FUNCT_2:def 2;

              then

               A47: (B * F) in <^o1, o^> by ALTCAT_1:def 14;

              (B . y) = ( IFEQ (y,y,l,k)) by A31, A39

              .= l by FUNCOP_1:def 8;

              then

               A48: not B = C by A31, A37, FUNCOP_1: 7;

              

               A49: ( dom (C * F)) = o1 by A27, A28, A33, RELAT_1: 27;

              now

                let z be object;

                assume

                 A50: z in o1;

                then

                 A51: (F . z) in ( rng F) by A27, FUNCT_1:def 3;

                

                then

                 A52: (B . (F . z)) = ( IFEQ ((F . z),y,l,k)) by A28, A39

                .= k by A32, A51, FUNCOP_1:def 8;

                

                thus ((B * F) . z) = (B . (F . z)) by A40, A50, FUNCT_1: 12

                .= (C . (F . z)) by A28, A51, A52, FUNCOP_1: 7

                .= ((C * F) . z) by A49, A50, FUNCT_1: 12;

              end;

              then (B * F) = (C * F) by A40, A49, FUNCT_1: 2;

              

              then (B1 * A) = (C * F) by A1, A2, A46, A47, ALTCAT_1: 16

              .= (C1 * A) by A1, A2, A46, A47, ALTCAT_1: 16;

              hence contradiction by A29, A48, A46;

            end;

            thus F is onto implies A is epi

            proof

              assume

               A53: F is onto;

              let o be Object of ( EnsCat X);

              assume

               A54: <^o2, o^> <> {} ;

              then

               A55: <^o1, o^> <> {} by A1, ALTCAT_1:def 2;

              let B,C be Morphism of o2, o;

              

               A56: <^o2, o^> = ( Funcs (o2,o)) by ALTCAT_1:def 14;

              then

              consider B1 be Function such that

               A57: B1 = B and

               A58: ( dom B1) = o2 and ( rng B1) c= o by A54, FUNCT_2:def 2;

              consider C1 be Function such that

               A59: C1 = C and

               A60: ( dom C1) = o2 and ( rng C1) c= o by A54, A56, FUNCT_2:def 2;

              assume (B * A) = (C * A);

              

              then

               A61: (B1 * F) = (C * A) by A1, A2, A54, A57, A55, ALTCAT_1: 16

              .= (C1 * F) by A1, A2, A54, A59, A55, ALTCAT_1: 16;

              now

                assume B1 <> C1;

                then

                consider z be object such that

                 A62: z in o2 and

                 A63: (B1 . z) <> (C1 . z) by A58, A60, FUNCT_1: 2;

                z in ( rng F) by A53, A62, FUNCT_2:def 3;

                then

                consider x be object such that

                 A64: x in ( dom F) and

                 A65: (F . x) = z by FUNCT_1:def 3;

                (B1 . (F . x)) = ((B1 * F) . x) by A64, FUNCT_1: 13;

                hence contradiction by A61, A63, A64, A65, FUNCT_1: 13;

              end;

              hence thesis by A57, A59;

            end;

          end;

            suppose

             A66: o2 = {} ;

            then F = {} ;

            hence A is epi implies F is onto by A66, FUNCT_2:def 3, RELAT_1: 38;

            thus F is onto implies A is epi

            proof

              assume F is onto;

              let o be Object of ( EnsCat X);

              assume

               A67: <^o2, o^> <> {} ;

              let B,C be Morphism of o2, o;

              

               A68: <^o2, o^> = ( Funcs (o2,o)) by ALTCAT_1:def 14;

              then

              consider B1 be Function such that

               A69: B1 = B and

               A70: ( dom B1) = o2 and ( rng B1) c= o by A67, FUNCT_2:def 2;

              

               A71: ex C1 be Function st C1 = C & ( dom C1) = o2 & ( rng C1) c= o by A67, A68, FUNCT_2:def 2;

              assume (B * A) = (C * A);

              B1 = {} by A66, A70, RELAT_1: 41;

              hence thesis by A66, A69, A71, RELAT_1: 41;

            end;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: ALTCAT_3:15

    

     Th15: for C be category, o1,o2 be Object of C st <^o1, o2^> <> {} & <^o2, o1^> <> {} holds for A be Morphism of o1, o2 st A is retraction holds A is epi

    proof

      let C be category, o1,o2 be Object of C;

      assume

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

      let A be Morphism of o1, o2;

      assume A is retraction;

      then

      consider R be Morphism of o2, o1 such that

       A2: R is_right_inverse_of A;

      let o be Object of C;

      assume

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

      let B,C be Morphism of o2, o;

      assume

       A4: (B * A) = (C * A);

      

      thus B = (B * ( idm o2)) by A3, ALTCAT_1:def 17

      .= (B * (A * R)) by A2

      .= ((C * A) * R) by A1, A3, A4, ALTCAT_1: 21

      .= (C * (A * R)) by A1, A3, ALTCAT_1: 21

      .= (C * ( idm o2)) by A2

      .= C by A3, ALTCAT_1:def 17;

    end;

    theorem :: ALTCAT_3:16

    

     Th16: for C be category, o1,o2 be Object of C st <^o1, o2^> <> {} & <^o2, o1^> <> {} holds for A be Morphism of o1, o2 st A is coretraction holds A is mono

    proof

      let C be category, o1,o2 be Object of C;

      assume

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

      let A be Morphism of o1, o2;

      assume A is coretraction;

      then

      consider R be Morphism of o2, o1 such that

       A2: R is_left_inverse_of A;

      let o be Object of C;

      assume

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

      let B,C be Morphism of o, o1;

      assume

       A4: (A * B) = (A * C);

      

      thus B = (( idm o1) * B) by A3, ALTCAT_1: 20

      .= ((R * A) * B) by A2

      .= (R * (A * C)) by A1, A3, A4, ALTCAT_1: 21

      .= ((R * A) * C) by A1, A3, ALTCAT_1: 21

      .= (( idm o1) * C) by A2

      .= C by A3, ALTCAT_1: 20;

    end;

    theorem :: ALTCAT_3:17

    for C be category, o1,o2 be Object of C st <^o1, o2^> <> {} & <^o2, o1^> <> {} holds for A be Morphism of o1, o2 st A is iso holds A is mono epi

    proof

      let C be category;

      let o1,o2 be Object of C such that

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

      let A be Morphism of o1, o2;

      assume A is iso;

      then

       A2: A is retraction & A is coretraction by A1, Th6;

      

       A3: for o be Object of C st <^o2, o^> <> {} holds for B,C be Morphism of o2, o st (B * A) = (C * A) holds B = C

      proof

        let o be Object of C such that

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

        let B,C be Morphism of o2, o;

        assume (B * A) = (C * A);

        then (B * (A * (A " ))) = ((C * A) * (A " )) by A1, A4, ALTCAT_1: 21;

        then (B * ( idm o2)) = ((C * A) * (A " )) by A1, A2, Th2;

        then (B * ( idm o2)) = (C * (A * (A " ))) by A1, A4, ALTCAT_1: 21;

        then (B * ( idm o2)) = (C * ( idm o2)) by A1, A2, Th2;

        then B = (C * ( idm o2)) by A4, ALTCAT_1:def 17;

        hence thesis by A4, ALTCAT_1:def 17;

      end;

      for o be Object of C st <^o, o1^> <> {} holds for B,C be Morphism of o, o1 st (A * B) = (A * C) holds B = C

      proof

        let o be Object of C such that

         A5: <^o, o1^> <> {} ;

        let B,C be Morphism of o, o1;

        assume (A * B) = (A * C);

        then (((A " ) * A) * B) = ((A " ) * (A * C)) by A1, A5, ALTCAT_1: 21;

        then (( idm o1) * B) = ((A " ) * (A * C)) by A1, A2, Th2;

        then (( idm o1) * B) = (((A " ) * A) * C) by A1, A5, ALTCAT_1: 21;

        then (( idm o1) * B) = (( idm o1) * C) by A1, A2, Th2;

        then B = (( idm o1) * C) by A5, ALTCAT_1: 20;

        hence thesis by A5, ALTCAT_1: 20;

      end;

      hence thesis by A3;

    end;

    theorem :: ALTCAT_3:18

    

     Th18: for C be category, o1,o2,o3 be Object of C st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o1^> <> {} holds for A be Morphism of o1, o2, B be Morphism of o2, o3 st A is retraction & B is retraction holds (B * A) is retraction

    proof

      let C be category, o1,o2,o3 be Object of C;

      assume that

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

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

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

      

       A4: <^o2, o1^> <> {} by A2, A3, ALTCAT_1:def 2;

      

       A5: <^o3, o2^> <> {} by A1, A3, ALTCAT_1:def 2;

      let A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume that

       A6: A is retraction and

       A7: B is retraction;

      consider A1 be Morphism of o2, o1 such that

       A8: A1 is_right_inverse_of A by A6;

      consider B1 be Morphism of o3, o2 such that

       A9: B1 is_right_inverse_of B by A7;

      consider G be Morphism of o3, o1 such that

       A10: G = (A1 * B1);

      take G;

      ((B * A) * G) = (B * (A * (A1 * B1))) by A1, A2, A3, A10, ALTCAT_1: 21

      .= (B * ((A * A1) * B1)) by A1, A4, A5, ALTCAT_1: 21

      .= (B * (( idm o2) * B1)) by A8

      .= (B * B1) by A5, ALTCAT_1: 20

      .= ( idm o3) by A9;

      hence thesis;

    end;

    theorem :: ALTCAT_3:19

    

     Th19: for C be category, o1,o2,o3 be Object of C st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o1^> <> {} holds for A be Morphism of o1, o2, B be Morphism of o2, o3 st A is coretraction & B is coretraction holds (B * A) is coretraction

    proof

      let C be category, o1,o2,o3 be Object of C;

      assume that

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

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

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

      

       A4: <^o2, o1^> <> {} by A2, A3, ALTCAT_1:def 2;

      

       A5: <^o3, o2^> <> {} by A1, A3, ALTCAT_1:def 2;

      let A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume that

       A6: A is coretraction and

       A7: B is coretraction;

      consider A1 be Morphism of o2, o1 such that

       A8: A1 is_left_inverse_of A by A6;

      consider B1 be Morphism of o3, o2 such that

       A9: B1 is_left_inverse_of B by A7;

      consider G be Morphism of o3, o1 such that

       A10: G = (A1 * B1);

      take G;

      

       A11: <^o2, o2^> <> {} by ALTCAT_1: 19;

      (G * (B * A)) = (((A1 * B1) * B) * A) by A1, A2, A3, A10, ALTCAT_1: 21

      .= ((A1 * (B1 * B)) * A) by A2, A4, A5, ALTCAT_1: 21

      .= ((A1 * ( idm o2)) * A) by A9

      .= (A1 * (( idm o2) * A)) by A1, A4, A11, ALTCAT_1: 21

      .= (A1 * A) by A1, ALTCAT_1: 20

      .= ( idm o1) by A8;

      hence thesis;

    end;

    theorem :: ALTCAT_3:20

    

     Th20: for C be category, o1,o2 be Object of C, A be Morphism of o1, o2 st A is retraction & A is mono & <^o1, o2^> <> {} & <^o2, o1^> <> {} holds A is iso

    proof

      let C be category, o1,o2 be Object of C, A be Morphism of o1, o2;

      assume that

       A1: A is retraction and

       A2: A is mono and

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

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

      consider B be Morphism of o2, o1 such that

       A5: B is_right_inverse_of A by A1;

      ((A * B) * A) = (( idm o2) * A) by A5;

      then (A * (B * A)) = (( idm o2) * A) by A3, A4, ALTCAT_1: 21;

      then (A * (B * A)) = A by A3, ALTCAT_1: 20;

      then

       A6: <^o1, o1^> <> {} & (A * (B * A)) = (A * ( idm o1)) by A3, ALTCAT_1: 19, ALTCAT_1:def 17;

      then (B * A) = ( idm o1) by A2;

      then

       A7: B is_left_inverse_of A;

      then

       A8: A is coretraction;

      

      then

       A9: (A * (A " )) = (A * B) by A1, A3, A4, A5, A7, Def4

      .= ( idm o2) by A5;

      ((A " ) * A) = (B * A) by A1, A3, A4, A5, A7, A8, Def4

      .= ( idm o1) by A2, A6;

      hence thesis by A9;

    end;

    theorem :: ALTCAT_3:21

    for C be category, o1,o2 be Object of C, A be Morphism of o1, o2 st A is coretraction & A is epi & <^o1, o2^> <> {} & <^o2, o1^> <> {} holds A is iso

    proof

      let C be category, o1,o2 be Object of C, A be Morphism of o1, o2;

      assume that

       A1: A is coretraction and

       A2: A is epi and

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

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

      consider B be Morphism of o2, o1 such that

       A5: B is_left_inverse_of A by A1;

      (A * (B * A)) = (A * ( idm o1)) by A5;

      then (A * (B * A)) = A by A3, ALTCAT_1:def 17;

      then (A * (B * A)) = (( idm o2) * A) by A3, ALTCAT_1: 20;

      then

       A6: <^o2, o2^> <> {} & ((A * B) * A) = (( idm o2) * A) by A3, A4, ALTCAT_1: 19, ALTCAT_1: 21;

      then (A * B) = ( idm o2) by A2;

      then

       A7: B is_right_inverse_of A;

      then

       A8: A is retraction;

      

      then

       A9: ((A " ) * A) = (B * A) by A1, A3, A4, A5, A7, Def4

      .= ( idm o1) by A5;

      (A * (A " )) = (A * B) by A1, A3, A4, A5, A7, A8, Def4

      .= ( idm o2) by A2, A6;

      hence thesis by A9;

    end;

    theorem :: ALTCAT_3:22

    for C be category, o1,o2,o3 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o3 st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o1^> <> {} & (B * A) is retraction holds B is retraction

    proof

      let C be category, o1,o2,o3 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume

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

      assume (B * A) is retraction;

      then

      consider G be Morphism of o3, o1 such that

       A2: G is_right_inverse_of (B * A);

      ((B * A) * G) = ( idm o3) by A2;

      then (B * (A * G)) = ( idm o3) by A1, ALTCAT_1: 21;

      then (A * G) is_right_inverse_of B;

      hence thesis;

    end;

    theorem :: ALTCAT_3:23

    for C be category, o1,o2,o3 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o3 st <^o1, o2^> <> {} & <^o2, o3^> <> {} & <^o3, o1^> <> {} & (B * A) is coretraction holds A is coretraction

    proof

      let C be category, o1,o2,o3 be Object of C, A be Morphism of o1, o2, B be Morphism of o2, o3;

      assume

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

      assume (B * A) is coretraction;

      then

      consider G be Morphism of o3, o1 such that

       A2: G is_left_inverse_of (B * A);

      

       A3: ((G * B) * A) = (G * (B * A)) by A1, ALTCAT_1: 21;

      (G * (B * A)) = ( idm o1) by A2;

      then (G * B) is_left_inverse_of A by A3;

      hence thesis;

    end;

    theorem :: ALTCAT_3:24

    for C be category st for o1,o2 be Object of C, A1 be Morphism of o1, o2 holds A1 is retraction holds for a,b be Object of C, A be Morphism of a, b st <^a, b^> <> {} & <^b, a^> <> {} holds A is iso

    proof

      let C be category;

      assume

       A1: for o1,o2 be Object of C, A1 be Morphism of o1, o2 holds A1 is retraction;

      thus for a,b be Object of C, A be Morphism of a, b st <^a, b^> <> {} & <^b, a^> <> {} holds A is iso

      proof

        let a,b be Object of C;

        let A be Morphism of a, b;

        assume that

         A2: <^a, b^> <> {} and

         A3: <^b, a^> <> {} ;

        

         A4: A is retraction by A1;

        A is coretraction

        proof

          consider A1 be Morphism of b, a such that

           A5: A1 is_right_inverse_of A by A4;

          (A1 * (A * A1)) = (A1 * ( idm b)) by A5;

          then (A1 * (A * A1)) = A1 by A3, ALTCAT_1:def 17;

          then ((A1 * A) * A1) = A1 by A2, A3, ALTCAT_1: 21;

          then

           A6: ((A1 * A) * A1) = (( idm a) * A1) by A3, ALTCAT_1: 20;

          A1 is epi & <^a, a^> <> {} by A1, A2, A3, Th15, ALTCAT_1: 19;

          then (A1 * A) = ( idm a) by A6;

          then A1 is_left_inverse_of A;

          hence thesis;

        end;

        hence thesis by A2, A3, A4, Th6;

      end;

    end;

    registration

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

      cluster mono epi retraction coretraction for Morphism of o, o;

      existence

      proof

        take ( idm o);

        thus thesis by Lm1, Th1;

      end;

    end

    registration

      let C be category, o be Object of C;

      cluster mono epi iso retraction coretraction for Morphism of o, o;

      existence

      proof

        take I = ( idm o);

         <^o, o^> <> {} & I is retraction coretraction by Th1, ALTCAT_1: 19;

        hence thesis by Th15, Th16, Th20;

      end;

    end

    registration

      let C be category, o be Object of C, A,B be mono Morphism of o, o;

      cluster (A * B) -> mono;

      coherence

      proof

         <^o, o^> <> {} by ALTCAT_1: 19;

        hence thesis by Th9;

      end;

    end

    registration

      let C be category, o be Object of C, A,B be epi Morphism of o, o;

      cluster (A * B) -> epi;

      coherence

      proof

         <^o, o^> <> {} by ALTCAT_1: 19;

        hence thesis by Th10;

      end;

    end

    registration

      let C be category, o be Object of C, A,B be iso Morphism of o, o;

      cluster (A * B) -> iso;

      coherence

      proof

         <^o, o^> <> {} by ALTCAT_1: 19;

        hence thesis by Th7;

      end;

    end

    registration

      let C be category, o be Object of C, A,B be retraction Morphism of o, o;

      cluster (A * B) -> retraction;

      coherence

      proof

         <^o, o^> <> {} by ALTCAT_1: 19;

        hence thesis by Th18;

      end;

    end

    registration

      let C be category, o be Object of C, A,B be coretraction Morphism of o, o;

      cluster (A * B) -> coretraction;

      coherence

      proof

         <^o, o^> <> {} by ALTCAT_1: 19;

        hence thesis by Th19;

      end;

    end

    definition

      let C be AltGraph, o be Object of C;

      :: ALTCAT_3:def9

      attr o is initial means for o1 be Object of C holds ex M be Morphism of o, o1 st M in <^o, o1^> & <^o, o1^> is trivial;

    end

    theorem :: ALTCAT_3:25

    for C be AltGraph, o be Object of C holds o is initial iff for o1 be Object of C holds ex M be Morphism of o, o1 st M in <^o, o1^> & for M1 be Morphism of o, o1 st M1 in <^o, o1^> holds M = M1

    proof

      let C be AltGraph, o be Object of C;

      thus o is initial implies for o1 be Object of C holds ex M be Morphism of o, o1 st M in <^o, o1^> & for M1 be Morphism of o, o1 st M1 in <^o, o1^> holds M = M1

      proof

        assume

         A1: o is initial;

        let o1 be Object of C;

        consider M be Morphism of o, o1 such that

         A2: M in <^o, o1^> and

         A3: <^o, o1^> is trivial by A1;

        ex i be object st <^o, o1^> = {i} by A2, A3, ZFMISC_1: 131;

        then <^o, o1^> = {M} by TARSKI:def 1;

        then for M1 be Morphism of o, o1 st M1 in <^o, o1^> holds M = M1 by TARSKI:def 1;

        hence thesis by A2;

      end;

      assume

       A4: for o1 be Object of C holds ex M be Morphism of o, o1 st M in <^o, o1^> & for M1 be Morphism of o, o1 st M1 in <^o, o1^> holds M = M1;

      let o1 be Object of C;

      consider M be Morphism of o, o1 such that

       A5: M in <^o, o1^> and

       A6: for M1 be Morphism of o, o1 st M1 in <^o, o1^> holds M = M1 by A4;

      

       A7: <^o, o1^> c= {M}

      proof

        let x be object;

        assume

         A8: x in <^o, o1^>;

        then

        reconsider M1 = x as Morphism of o, o1;

        M1 = M by A6, A8;

        hence thesis by TARSKI:def 1;

      end;

       {M} c= <^o, o1^> by A5, TARSKI:def 1;

      then <^o, o1^> = {M} by A7, XBOOLE_0:def 10;

      hence thesis;

    end;

    theorem :: ALTCAT_3:26

    

     Th26: for C be category, o1,o2 be Object of C st o1 is initial & o2 is initial holds (o1,o2) are_iso

    proof

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

       A1: o1 is initial and

       A2: o2 is initial;

      ex N be Morphism of o2, o2 st N in <^o2, o2^> & <^o2, o2^> is trivial by A2;

      then

      consider y be object such that

       A3: <^o2, o2^> = {y} by ZFMISC_1: 131;

      consider M2 be Morphism of o2, o1 such that

       A4: M2 in <^o2, o1^> and <^o2, o1^> is trivial by A2;

      consider M1 be Morphism of o1, o2 such that

       A5: M1 in <^o1, o2^> and <^o1, o2^> is trivial by A1;

      thus <^o1, o2^> <> {} & <^o2, o1^> <> {} by A5, A4;

      (M1 * M2) = y & ( idm o2) = y by A3, TARSKI:def 1;

      then M2 is_right_inverse_of M1;

      then

       A6: M1 is retraction;

      ex M be Morphism of o1, o1 st M in <^o1, o1^> & <^o1, o1^> is trivial by A1;

      then

      consider x be object such that

       A7: <^o1, o1^> = {x} by ZFMISC_1: 131;

      (M2 * M1) = x & ( idm o1) = x by A7, TARSKI:def 1;

      then M2 is_left_inverse_of M1;

      then M1 is coretraction;

      then M1 is iso by A5, A4, A6, Th6;

      hence thesis;

    end;

    definition

      let C be AltGraph, o be Object of C;

      :: ALTCAT_3:def10

      attr o is terminal means for o1 be Object of C holds ex M be Morphism of o1, o st M in <^o1, o^> & <^o1, o^> is trivial;

    end

    theorem :: ALTCAT_3:27

    for C be AltGraph, o be Object of C holds o is terminal iff for o1 be Object of C holds ex M be Morphism of o1, o st M in <^o1, o^> & for M1 be Morphism of o1, o st M1 in <^o1, o^> holds M = M1

    proof

      let C be AltGraph, o be Object of C;

      thus o is terminal implies for o1 be Object of C holds ex M be Morphism of o1, o st M in <^o1, o^> & for M1 be Morphism of o1, o st M1 in <^o1, o^> holds M = M1

      proof

        assume

         A1: o is terminal;

        let o1 be Object of C;

        consider M be Morphism of o1, o such that

         A2: M in <^o1, o^> and

         A3: <^o1, o^> is trivial by A1;

        ex i be object st <^o1, o^> = {i} by A2, A3, ZFMISC_1: 131;

        then <^o1, o^> = {M} by TARSKI:def 1;

        then for M1 be Morphism of o1, o st M1 in <^o1, o^> holds M = M1 by TARSKI:def 1;

        hence thesis by A2;

      end;

      assume

       A4: for o1 be Object of C holds ex M be Morphism of o1, o st M in <^o1, o^> & for M1 be Morphism of o1, o st M1 in <^o1, o^> holds M = M1;

      let o1 be Object of C;

      consider M be Morphism of o1, o such that

       A5: M in <^o1, o^> and

       A6: for M1 be Morphism of o1, o st M1 in <^o1, o^> holds M = M1 by A4;

      

       A7: <^o1, o^> c= {M}

      proof

        let x be object;

        assume

         A8: x in <^o1, o^>;

        then

        reconsider M1 = x as Morphism of o1, o;

        M1 = M by A6, A8;

        hence thesis by TARSKI:def 1;

      end;

       {M} c= <^o1, o^> by A5, TARSKI:def 1;

      then <^o1, o^> = {M} by A7, XBOOLE_0:def 10;

      hence thesis;

    end;

    theorem :: ALTCAT_3:28

    for C be category, o1,o2 be Object of C st o1 is terminal & o2 is terminal holds (o1,o2) are_iso

    proof

      let C be category, o1,o2 be Object of C;

      assume that

       A1: o1 is terminal and

       A2: o2 is terminal;

      ex M be Morphism of o1, o1 st M in <^o1, o1^> & <^o1, o1^> is trivial by A1;

      then

      consider x be object such that

       A3: <^o1, o1^> = {x} by ZFMISC_1: 131;

      consider M2 be Morphism of o2, o1 such that

       A4: M2 in <^o2, o1^> and <^o2, o1^> is trivial by A1;

      consider M1 be Morphism of o1, o2 such that

       A5: M1 in <^o1, o2^> and <^o1, o2^> is trivial by A2;

      thus <^o1, o2^> <> {} & <^o2, o1^> <> {} by A5, A4;

      (M2 * M1) = x by A3, TARSKI:def 1;

      then (M2 * M1) = ( idm o1) by A3, TARSKI:def 1;

      then M2 is_left_inverse_of M1;

      then

       A6: M1 is coretraction;

      ex N be Morphism of o2, o2 st N in <^o2, o2^> & <^o2, o2^> is trivial by A2;

      then

      consider y be object such that

       A7: <^o2, o2^> = {y} by ZFMISC_1: 131;

      (M1 * M2) = y by A7, TARSKI:def 1;

      then (M1 * M2) = ( idm o2) by A7, TARSKI:def 1;

      then M2 is_right_inverse_of M1;

      then M1 is retraction;

      then M1 is iso by A5, A4, A6, Th6;

      hence thesis;

    end;

    definition

      let C be AltGraph, o be Object of C;

      :: ALTCAT_3:def11

      attr o is _zero means o is initial terminal;

    end

    theorem :: ALTCAT_3:29

    for C be category, o1,o2 be Object of C st o1 is _zero & o2 is _zero holds (o1,o2) are_iso by Th26;

    definition

      let C be non empty AltCatStr, o1,o2 be Object of C, M be Morphism of o1, o2;

      :: ALTCAT_3:def12

      attr M is _zero means for o be Object of C st o is _zero holds for A be Morphism of o1, o, B be Morphism of o, o2 holds M = (B * A);

    end

    theorem :: ALTCAT_3:30

    for C be category, o1,o2,o3 be Object of C holds for M1 be Morphism of o1, o2, M2 be Morphism of o2, o3 st M1 is _zero & M2 is _zero holds (M2 * M1) is _zero

    proof

      let C be category, o1,o2,o3 be Object of C, M1 be Morphism of o1, o2, M2 be Morphism of o2, o3;

      assume that

       A1: M1 is _zero and

       A2: M2 is _zero;

      let o be Object of C;

      assume

       A3: o is _zero;

      then

       A4: o is initial;

      then

      consider B1 be Morphism of o, o2 such that

       A5: B1 in <^o, o2^> and <^o, o2^> is trivial;

      let A be Morphism of o1, o, B be Morphism of o, o3;

      consider B2 be Morphism of o, o3 such that

       A6: B2 in <^o, o3^> and

       A7: <^o, o3^> is trivial by A4;

      consider y be object such that

       A8: <^o, o3^> = {y} by A6, A7, ZFMISC_1: 131;

      

       A9: o is terminal by A3;

      then

      consider A1 be Morphism of o1, o such that

       A10: A1 in <^o1, o^> and

       A11: <^o1, o^> is trivial;

      consider x be object such that

       A12: <^o1, o^> = {x} by A10, A11, ZFMISC_1: 131;

      ex M be Morphism of o, o st M in <^o, o^> & <^o, o^> is trivial by A9;

      then

      consider z be object such that

       A13: <^o, o^> = {z} by ZFMISC_1: 131;

      consider A2 be Morphism of o2, o such that

       A14: A2 in <^o2, o^> and <^o2, o^> is trivial by A9;

      

       A15: ( idm o) = z & (A2 * B1) = z by A13, TARSKI:def 1;

      

       A16: B = y & B2 = y by A8, TARSKI:def 1;

      

       A17: A = x & A1 = x by A12, TARSKI:def 1;

      

       A18: <^o2, o3^> <> {} by A6, A14, ALTCAT_1:def 2;

      M2 = (B2 * A2) by A2, A3;

      

      hence (M2 * M1) = ((B2 * A2) * (B1 * A1)) by A1, A3

      .= (((B2 * A2) * B1) * A1) by A5, A10, A18, ALTCAT_1: 21

      .= ((B * ( idm o)) * A) by A5, A6, A14, A17, A16, A15, ALTCAT_1: 21

      .= (B * A) by A6, ALTCAT_1:def 17;

    end;