oppcat_1.miz



    begin

    reserve B,C,D for Category;

    definition

      let C;

      :: OPPCAT_1:def1

      func C opp -> strict non empty non void CatStr equals CatStr (# the carrier of C, the carrier' of C, the Target of C, the Source of C, ( ~ the Comp of C) #);

      coherence ;

    end

    definition

      let C;

      let c be Object of C;

      :: OPPCAT_1:def2

      func c opp -> Object of (C opp ) equals c;

      coherence ;

    end

    registration

      let C;

      cluster (C opp ) -> Category-like transitive associative reflexive with_identities;

      coherence

      proof

        set M = the carrier' of C, d = the Target of C, c = the Source of C, p = ( ~ the Comp of C);

        set B = (C opp );

        thus

         A1: B is Category-like

        proof

          let f,g be Morphism of B;

          reconsider ff = f, gg = g as Morphism of C;

          thus [g, f] in ( dom the Comp of B) implies ( dom g) = ( cod f)

          proof

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

            then [ff, gg] in ( dom the Comp of C) by FUNCT_4: 42;

            then ( dom ff) = ( cod gg) by CAT_1:def 6;

            hence ( dom g) = ( cod f);

          end;

          assume

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

          ( cod gg) = ( dom ff) by A2;

          then [ff, gg] in ( dom the Comp of C) by CAT_1:def 6;

          hence [g, f] in ( dom the Comp of B) by FUNCT_4: 42;

        end;

        

         A3: for f,g be Element of M st (d . g) = (c . f) holds (p . (g,f)) = (the Comp of C . (f,g))

        proof

          let f,g be Element of M;

          reconsider ff = f, gg = g as Morphism of B;

          assume (d . g) = (c . f);

          then ( dom gg) = ( cod ff);

          then [gg, ff] in ( dom p) by A1;

          hence thesis by FUNCT_4: 43;

        end;

        thus

         A4: B is transitive

        proof

          let ff,gg be Morphism of B;

          reconsider f = ff, g = gg as Morphism of C;

          assume

           A5: ( dom gg) = ( cod ff);

          then

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

          then

           A7: [f, g] in ( dom the Comp of C) by CAT_1:def 6;

           [gg, ff] in ( dom the Comp of B) by A5, A1;

          

          then

           A8: (gg (*) ff) = (p . (g,f)) by CAT_1:def 1

          .= (the Comp of C . (f,g)) by A3, A5

          .= (f (*) g) by A7, CAT_1:def 1;

          

          hence ( dom (gg (*) ff)) = ( cod (f (*) g))

          .= ( cod f) by A6, CAT_1:def 7

          .= ( dom ff);

          

          thus ( cod (gg (*) ff)) = ( dom (f (*) g)) by A8

          .= ( dom g) by A6, CAT_1:def 7

          .= ( cod gg);

        end;

        thus B is associative

        proof

          let ff,gg,hh be Morphism of B;

          reconsider f = ff, g = gg, h = hh as Morphism of C;

          assume that

           A9: ( dom hh) = ( cod gg) and

           A10: ( dom gg) = ( cod ff);

          

           A11: [h, g] in ( dom p) by A1, A9;

          then

           A12: (p . (h,g)) is Element of M by PARTFUN1: 4;

          

           A13: [g, f] in ( dom p) by A1, A10;

          then

           A14: (p . (g,f)) is Element of M by PARTFUN1: 4;

          

           A15: (p . (h,g)) = (the Comp of C . (g,h)) by A3, A9;

          (d . (p . (h,g))) = ( dom (hh (*) gg)) by A11, CAT_1:def 1

          .= ( dom gg) by A4, A9;

          then

           A16: (p . ((p . (h,g)),f)) = (the Comp of C . (f,(the Comp of C . (g,h)))) by A3, A10, A12, A15;

          

           A17: ( cod h) = ( dom g) & ( cod g) = ( dom f) by A9, A10;

          

           A18: (p . (g,f)) = (the Comp of C . (f,g)) by A3, A10;

          

           A19: (c . (p . (g,f))) = ( cod (gg (*) ff)) by A13, CAT_1:def 1

          .= ( cod gg) by A4, A10;

          ( dom (hh (*) gg)) = ( dom gg) by A4, A9;

          then

           A20: [(hh (*) gg), ff] in ( dom the Comp of B) by A1, A10;

          ( cod (gg (*) ff)) = ( cod gg) by A4, A10;

          then

           A21: [hh, (gg (*) ff)] in ( dom the Comp of B) by A1, A9;

           [hh, gg] in ( dom the Comp of B) by A9, A1;

          then

           A22: (hh (*) gg) = (p . (h,g)) by CAT_1:def 1;

          

           A23: (f (*) g) = (the Comp of C . (f,g)) by A17, CAT_1: 16;

          

           A24: ( dom (f (*) g)) = ( dom g) by A17, CAT_1:def 7;

          

           A25: (g (*) h) = (the Comp of C . (g,h)) by A17, CAT_1: 16;

          

           A26: ( cod (g (*) h)) = ( cod g) by A17, CAT_1:def 7;

           [gg, ff] in ( dom the Comp of B) by A10, A1;

          then (gg (*) ff) = (p . (g,f)) by CAT_1:def 1;

          

          hence (hh (*) (gg (*) ff)) = (p . (h,(p . (g,f)))) by A21, CAT_1:def 1

          .= (the Comp of C . ((the Comp of C . (f,g)),h)) by A3, A9, A14, A18, A19

          .= ((f (*) g) (*) h) by A23, A17, A24, CAT_1: 16

          .= (f (*) (g (*) h)) by A17, CAT_1:def 8

          .= (p . ((p . (h,g)),f)) by A16, A17, A25, A26, CAT_1: 16

          .= ((hh (*) gg) (*) ff) by A20, A22, CAT_1:def 1;

        end;

        thus B is reflexive

        proof

          let bb be Object of B;

          reconsider b = bb as Element of C;

          consider f be Morphism of C such that

           A27: f in ( Hom (b,b)) by SUBSET_1: 4;

          reconsider ff = f as Morphism of B;

          

           A28: ( dom ff) = ( cod f)

          .= bb by A27, CAT_1: 1;

          ( cod ff) = ( dom f)

          .= bb by A27, CAT_1: 1;

          then ff in ( Hom (bb,bb)) by A28;

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

        end;

        let a be Element of B;

        reconsider aa = a as Element of C;

        reconsider ii = ( id aa) as Morphism of B;

        

         A29: ( dom ii) = ( cod ( id aa))

        .= aa;

        

         A30: ( cod ii) = ( dom ( id aa))

        .= aa;

        then

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

        take ii;

        let b be Element of B;

        reconsider bb = b as Element of C;

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

        proof

          assume

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

          let g be Morphism of a, b;

          reconsider gg = g as Morphism of C;

          

           A32: ( dom gg) = ( cod g)

          .= bb by A31, CAT_1: 5;

          

           A33: ( cod gg) = ( dom g)

          .= aa by A31, CAT_1: 5;

          then

           A34: ( cod gg) = ( dom ( id aa));

          reconsider gg as Morphism of bb, aa by A32, A33, CAT_1: 4;

          

           A35: (c . ii) = aa by A30

          .= ( dom g) by A31, CAT_1: 5

          .= (d . g);

          then ( dom g) = ( cod ii);

          then [g, ii] in ( dom the Comp of B) by A1;

          

          hence (g (*) ii) = (p . (g,ii)) by CAT_1:def 1

          .= (the Comp of C . (ii,g)) by A35, A3

          .= (( id aa) (*) gg) by A34, CAT_1: 16

          .= g by A33, CAT_1: 21;

        end;

        assume

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

        let g be Morphism of b, a;

        reconsider gg = g as Morphism of C;

        

         A37: ( cod gg) = ( dom g)

        .= bb by A36, CAT_1: 5;

        

         A38: ( dom gg) = ( cod g)

        .= aa by A36, CAT_1: 5;

        then

         A39: ( dom gg) = ( cod ( id aa));

        reconsider gg as Morphism of aa, bb by A37, A38, CAT_1: 4;

        

         A40: (d . ii) = aa by A29

        .= ( cod g) by A36, CAT_1: 5

        .= (c . g);

        then ( cod g) = ( dom ii);

        then [ii, g] in ( dom the Comp of B) by A1;

        

        hence (ii (*) g) = (p . (ii,g)) by CAT_1:def 1

        .= (the Comp of C . (g,ii)) by A40, A3

        .= (gg (*) ( id aa)) by A39, CAT_1: 16

        .= g by A38, CAT_1: 22;

      end;

    end

    definition

      let C;

      let c be Object of (C opp );

      :: OPPCAT_1:def3

      func opp c -> Object of C equals (c opp );

      coherence ;

    end

    ::$Canceled

    theorem :: OPPCAT_1:2

    for c be Object of C holds ((c opp ) opp ) = c;

    theorem :: OPPCAT_1:3

    for c be Object of C holds ( opp (c opp )) = c;

    theorem :: OPPCAT_1:4

    for c be Object of (C opp ) holds (( opp c) opp ) = c;

    theorem :: OPPCAT_1:5

    

     Th4: for a,b be Object of C holds ( Hom (a,b)) = ( Hom ((b opp ),(a opp )))

    proof

      let a,b be Object of C;

      thus ( Hom (a,b)) c= ( Hom ((b opp ),(a opp )))

      proof

        let x be object;

        assume

         A1: x in ( Hom (a,b));

        then

        reconsider f = x as Morphism of C;

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

        ( dom f) = a & ( cod f) = b by A1, CAT_1: 1;

        then ( dom g) = (b opp ) & ( cod g) = (a opp );

        hence x in ( Hom ((b opp ),(a opp )));

      end;

      let x be object;

      assume

       A2: x in ( Hom ((b opp ),(a opp )));

      then

      reconsider f = x as Morphism of (C opp );

      reconsider g = f as Morphism of C;

      ( dom f) = (b opp ) & ( cod f) = (a opp ) by A2, CAT_1: 1;

      then ( dom g) = a & ( cod g) = b;

      hence x in ( Hom (a,b));

    end;

    theorem :: OPPCAT_1:6

    

     Th5: for a,b be Object of (C opp ) holds ( Hom (a,b)) = ( Hom (( opp b),( opp a)))

    proof

      let a,b be Object of (C opp );

      

      thus ( Hom (a,b)) = ( Hom ((( opp a) opp ),(( opp b) opp )))

      .= ( Hom (( opp b),( opp a))) by Th4;

    end;

    definition

      let C;

      let f be Morphism of C;

      :: OPPCAT_1:def4

      func f opp -> Morphism of (C opp ) equals f;

      coherence ;

    end

    definition

      let C;

      let f be Morphism of (C opp );

      :: OPPCAT_1:def5

      func opp f -> Morphism of C equals (f opp );

      coherence ;

    end

    definition

      let C;

      let a,b be Object of C;

      let f be Morphism of a, b;

      :: OPPCAT_1:def6

      func f opp -> Morphism of (b opp ), (a opp ) equals

      : Def6: f;

      coherence

      proof

        f in ( Hom (a,b)) by A1, CAT_1:def 5;

        then f in ( Hom ((b opp ),(a opp ))) by Th4;

        hence thesis by CAT_1:def 5;

      end;

    end

    definition

      let C;

      let a,b be Object of C;

      let f be Morphism of (a opp ), (b opp );

      :: OPPCAT_1:def7

      func opp f -> Morphism of b, a equals

      : Def7: f;

      coherence

      proof

        f in ( Hom ((a opp ),(b opp ))) by A1, CAT_1:def 5;

        then f in ( Hom (b,a)) by Th4;

        hence thesis by CAT_1:def 5;

      end;

    end

    theorem :: OPPCAT_1:7

    for a,b be Object of C st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((f opp ) opp ) = f

    proof

      let a,b be Object of C;

      assume

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

      then

       A2: ( Hom ((b opp ),(a opp ))) <> {} by Th4;

      let f be Morphism of a, b;

      

      thus ((f opp ) opp ) = (f opp ) by A2, Def6

      .= f by A1, Def6;

    end;

    theorem :: OPPCAT_1:8

    for a,b be Object of C st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ( opp (f opp )) = f

    proof

      let a,b be Object of C;

      assume

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

      then

       A2: ( Hom ((b opp ),(a opp ))) <> {} by Th4;

      let f be Morphism of a, b;

      

      thus ( opp (f opp )) = (f opp ) by A2, Def7

      .= f by A1, Def6;

    end;

    theorem :: OPPCAT_1:9

    for a,b be Object of (C opp ) holds for f be Morphism of a, b holds (( opp f) opp ) = f;

    theorem :: OPPCAT_1:10

    

     Th9: for a,b be Object of C st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ( dom (f opp )) = ( cod f) & ( cod (f opp )) = ( dom f)

    proof

      let a,b be Object of C;

      assume

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

      then

       A2: ( Hom ((b opp ),(a opp ))) <> {} by Th4;

      let f be Morphism of a, b;

      

      thus ( dom (f opp )) = b by A2, CAT_1: 5

      .= ( cod f) by A1, CAT_1: 5;

      

      thus ( cod (f opp )) = a by A2, CAT_1: 5

      .= ( dom f) by A1, CAT_1: 5;

    end;

    theorem :: OPPCAT_1:11

    for a,b be Object of (C opp ) holds for f be Morphism of a, b holds ( dom ( opp f)) = ( cod f) & ( cod ( opp f)) = ( dom f);

    theorem :: OPPCAT_1:12

    for a,b be Object of C st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (( dom f) opp ) = ( cod (f opp )) & (( cod f) opp ) = ( dom (f opp )) by Th9;

    theorem :: OPPCAT_1:13

    for a,b be Object of (C opp ) st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ( opp ( dom f)) = ( cod ( opp f)) & ( opp ( cod f)) = ( dom ( opp f));

    ::$Canceled

    theorem :: OPPCAT_1:15

    

     Th13: for a,b be Object of (C opp ), f be Morphism of a, b st ( Hom (a,b)) <> {} holds ( opp f) is Morphism of ( opp b), ( opp a)

    proof

      let a,b be Object of (C opp ), f be Morphism of a, b;

      assume ( Hom (a,b)) <> {} ;

      then f in ( Hom (a,b)) by CAT_1:def 5;

      then ( opp f) in ( Hom (( opp b),( opp a))) by Th5;

      hence thesis by CAT_1:def 5;

    end;

    theorem :: OPPCAT_1:16

    

     Th14: for a,b,c be Object of C st ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds ((g (*) f) opp ) = ((f opp ) (*) (g opp ))

    proof

      let a,b,c be Object of C such that

       A1: ( Hom (a,b)) <> {} and

       A2: ( Hom (b,c)) <> {} ;

      

       A3: ( Hom ((b opp ),(a opp ))) <> {} by A1, Th4;

      

       A4: ( Hom ((c opp ),(b opp ))) <> {} by A2, Th4;

      let f be Morphism of a, b, g be Morphism of b, c;

      

       A5: ( dom g) = b by A2, CAT_1: 5

      .= ( cod f) by A1, CAT_1: 5;

      then

       A6: (g (*) f) = (the Comp of C . (g,f)) by CAT_1: 16;

      

       A7: (f opp ) = f & (g opp ) = g by A1, A2, Def6;

      

       A8: ( dom g) = (b opp ) by A2, CAT_1: 5

      .= ( cod (g opp )) by A4, CAT_1: 5;

      

       A9: ( cod f) = (b opp ) by A1, CAT_1: 5

      .= ( dom (f opp )) by A3, CAT_1: 5;

      then the Comp of C = ( ~ the Comp of (C opp )) & [(f opp ), (g opp )] in ( dom the Comp of (C opp )) by A5, A8, CAT_1: 15, FUNCT_4: 53;

      then (the Comp of C . (g,f)) = (the Comp of (C opp ) . ((f opp ),(g opp ))) by A7, FUNCT_4:def 2;

      hence thesis by A5, A6, A8, A9, CAT_1: 16;

    end;

    theorem :: OPPCAT_1:17

    for a,b,c be Object of C st ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((c opp ),(b opp ))) <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds ((g (*) f) opp ) = ((f opp ) (*) (g opp ))

    proof

      let a,b,c be Object of C;

      assume ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((c opp ),(b opp ))) <> {} ;

      then ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} by Th4;

      hence thesis by Th14;

    end;

    theorem :: OPPCAT_1:18

    

     Th16: for f,g be Morphism of (C opp ) st ( dom g) = ( cod f) holds ( opp (g (*) f)) = (( opp f) (*) ( opp g))

    proof

      let f,g be Morphism of (C opp );

      assume

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

      

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

      then

       A3: [( opp f), ( opp g)] in ( dom the Comp of C) by A1, CAT_1: 15;

      

      thus ( opp (g (*) f)) = (( ~ the Comp of C) . (( opp g),( opp f))) by A1, CAT_1: 16

      .= (the Comp of C . (( opp f),( opp g))) by A3, FUNCT_4:def 2

      .= (( opp f) (*) ( opp g)) by A1, A2, CAT_1: 16;

    end;

    theorem :: OPPCAT_1:19

    for a,b,c be Object of C, f be Morphism of a, b, g be Morphism of b, c st ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} holds ((g * f) opp ) = ((f opp ) (*) (g opp ))

    proof

      let a,b,c be Object of C, f be Morphism of a, b, g be Morphism of b, c;

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} ;

      

       A2: ( Hom (a,c)) <> {} by A1, CAT_1: 24;

      

      thus ((g * f) opp ) = (g * f) by A2, Def6

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

      .= ((f opp ) (*) (g opp )) by A1, Th14;

    end;

    

     Lm1: for a be Object of C holds for b be Object of (C opp ) holds (( Hom ((a opp ),b)) <> {} implies for f be Morphism of (a opp ), b holds (f (*) (( id a) opp )) = f) & (( Hom (b,(a opp ))) <> {} implies for f be Morphism of b, (a opp ) holds ((( id a) opp ) (*) f) = f)

    proof

      let a be Object of C;

      let b be Object of (C opp );

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

      proof

        assume

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

        

         A2: ( Hom (( opp b),( opp (a opp )))) <> {} by A1, Th5;

        let f be Morphism of (a opp ), b;

        

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

        

         A4: ( cod ( opp f qua Morphism of (C opp ))) = ( dom f)

        .= a by A1, CAT_1: 5;

        ( dom ( opp f qua Morphism of (C opp ))) = ( cod f)

        .= ( opp b) by A1, CAT_1: 5;

        then

        reconsider ff = ( opp f) as Morphism of ( opp b), a by A4, CAT_1: 4;

        

         A5: (( id a) (*) ff) = (( id a) * ff) by A3, A2, CAT_1:def 13;

        

        thus (f (*) (( id a) opp )) = ((ff opp ) (*) (( id a) opp )) by A2, Def6

        .= ((( id a) (*) ff) opp ) by A2, A3, Th14

        .= ((( id a) * ff) opp ) by A5, Def6, A2

        .= (ff opp ) by A2, CAT_1: 28

        .= f by A2, Def6;

      end;

      assume

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

      

       A7: ( Hom (( opp (a opp )),( opp b))) <> {} by A6, Th5;

      let f be Morphism of b, (a opp );

      

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

      

       A9: ( dom ( opp f qua Morphism of (C opp ))) = ( cod f)

      .= a by A6, CAT_1: 5;

      ( cod ( opp f qua Morphism of (C opp ))) = ( dom f)

      .= ( opp b) by A6, CAT_1: 5;

      then

      reconsider ff = ( opp f qua Morphism of (C opp )) as Morphism of a, ( opp b) by A9, CAT_1: 4;

      

       A10: (ff (*) ( id a)) = (ff * ( id a)) by A8, A7, CAT_1:def 13;

      

      thus ((( id a) opp ) (*) f) = ((( id a) opp ) (*) (ff opp )) by A7, Def6

      .= ((ff (*) ( id a)) opp ) by A8, A7, Th14

      .= ((ff * ( id a)) opp ) by A10, Def6, A7

      .= (ff opp ) by A7, CAT_1: 29

      .= f by A7, Def6;

    end;

    theorem :: OPPCAT_1:20

    

     Th18: for a be Object of C holds (( id a) opp ) = ( id (a opp ))

    proof

      let a be Object of C;

      for b be Object of (C opp ) holds (( Hom ((a opp ),b)) <> {} implies for f be Morphism of (a opp ), b holds (f (*) (( id a) opp )) = f) & (( Hom (b,(a opp ))) <> {} implies for f be Morphism of b, (a opp ) holds ((( id a) opp ) (*) f) = f) by Lm1;

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

    end;

    

     Lm2: for a be Object of C holds ( id a) = ( id (a opp ))

    proof

      let a be Object of C;

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

      

      hence ( id a) = (( id a) opp ) by Def6

      .= ( id (a opp )) by Th18;

    end;

    theorem :: OPPCAT_1:21

    

     Th19: for a be Object of (C opp ) holds ( opp ( id a)) = ( id ( opp a))

    proof

      let a be Object of (C opp );

      set b = ( opp a);

      

      thus ( opp ( id a)) = ( id (b opp ))

      .= ( id ( opp a)) by Lm2;

    end;

    

     Lm3: for a,b,c be Object of C st ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds (g * f) = ((f opp ) * (g opp ))

    proof

      let a,b,c be Object of C such that

       A1: ( Hom (a,b)) <> {} and

       A2: ( Hom (b,c)) <> {} ;

      let f be Morphism of a, b, g be Morphism of b, c;

      reconsider f1 = f as Morphism of C;

      reconsider g1 = g as Morphism of C;

      

       A3: ( Hom ((b opp ),(a opp ))) <> {} by A1, Th4;

      

       A4: ( Hom ((c opp ),(b opp ))) <> {} by A2, Th4;

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

      .= ((f opp ) (*) (g opp )) by A1, A2, Th14

      .= ((f opp ) * (g opp )) by A3, A4, CAT_1:def 13;

      hence thesis;

    end;

    theorem :: OPPCAT_1:22

    for a,b be Object of C holds for f be Morphism of a, b holds (f opp ) is monic iff f is epi

    proof

      let a,b be Object of C;

      let f be Morphism of a, b;

      thus (f opp ) is monic implies f is epi

      proof

        assume that

         A1: ( Hom ((b opp ),(a opp ))) <> {} and

         A2: for c be Object of (C opp ) st ( Hom (c,(b opp ))) <> {} holds for f1,f2 be Morphism of c, (b opp ) st ((f opp ) * f1) = ((f opp ) * f2) holds f1 = f2;

        thus

         A3: ( Hom (a,b)) <> {} by A1, Th4;

        let c be Object of C such that

         A4: ( Hom (b,c)) <> {} ;

        let g1,g2 be Morphism of b, c;

        assume

         A5: (g1 * f) = (g2 * f);

        reconsider f1 = (g1 opp ), f2 = (g2 opp ) as Morphism of (c opp ), (b opp );

        

         A6: ( Hom ((c opp ),(b opp ))) <> {} by A4, Th4;

        ((f opp ) * f1) = (g1 * f) by A4, Lm3, A3

        .= ((f opp ) * f2) by A4, Lm3, A3, A5;

        then

         A7: f1 = f2 by A2, A6;

        g1 = f1 by A4, Def6

        .= g2 by A7, A4, Def6;

        hence thesis;

      end;

      assume that

       A8: ( Hom (a,b)) <> {} and

       A9: for c be Object of C st ( Hom (b,c)) <> {} holds for g1,g2 be Morphism of b, c st (g1 * f) = (g2 * f) holds g1 = g2;

      thus ( Hom ((b opp ),(a opp ))) <> {} by A8, Th4;

      let c be Object of (C opp ) such that

       A10: ( Hom (c,(b opp ))) <> {} ;

      let f1,f2 be Morphism of c, (b opp );

      assume

       A11: ((f opp ) * f1) = ((f opp ) * f2);

      f1 in ( Hom (c,(b opp ))) & f2 in ( Hom (c,(b opp ))) by A10, CAT_1:def 5;

      then f1 in ( Hom (( opp (b opp )),( opp c))) & f2 in ( Hom (( opp (b opp )),( opp c))) by Th5;

      then

      reconsider g1 = ( opp f1), g2 = ( opp f2) as Morphism of b, ( opp c) by CAT_1:def 5;

      

       A12: ( Hom (( opp (b opp )),( opp c))) <> {} by A10, Th5;

      

       A13: (g1 opp ) = f1 by Def6, A12;

      

       A14: (g2 opp ) = f2 by Def6, A12;

      (g1 * f) = ((f opp ) * f2) by A11, A13, A8, Lm3, A12

      .= (g2 * f) by A8, Lm3, A12, A14;

      hence f1 = f2 by A9, A12;

    end;

    theorem :: OPPCAT_1:23

    for b,c be Object of C st ( Hom (b,c)) <> {} holds for f be Morphism of b, c holds (f opp ) is epi iff f is monic

    proof

      let b,c be Object of C such that

       A1: ( Hom (b,c)) <> {} ;

      let f be Morphism of b, c;

      thus (f opp ) is epi implies f is monic

      proof

        assume that ( Hom ((c opp ),(b opp ))) <> {} and

         A2: for a be Object of (C opp ) st ( Hom ((b opp ),a)) <> {} holds for g1,g2 be Morphism of (b opp ), a st (g1 * (f opp )) = (g2 * (f opp )) holds g1 = g2;

        thus ( Hom (b,c)) <> {} by A1;

        let a be Object of C such that

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

        let f1,f2 be Morphism of a, b;

        assume

         A4: (f * f1) = (f * f2);

        reconsider g1 = (f1 opp ), g2 = (f2 opp ) as Morphism of (b opp ), (a opp );

        

         A5: ( Hom ((b opp ),(a opp ))) <> {} by A3, Th4;

        (g1 * (f opp )) = (f * f1) by Lm3, A1, A3

        .= (g2 * (f opp )) by Lm3, A1, A3, A4;

        then g1 = g2 by A2, A5;

        

        hence f1 = g2 by Def6, A3

        .= f2 by Def6, A3;

      end;

      assume that

       A6: ( Hom (b,c)) <> {} and

       A7: for a be Object of C st ( Hom (a,b)) <> {} holds for f1,f2 be Morphism of a, b st (f * f1) = (f * f2) holds f1 = f2;

      thus ( Hom ((c opp ),(b opp ))) <> {} by A6, Th4;

      let a be Object of (C opp ) such that

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

      let g1,g2 be Morphism of (b opp ), a;

      assume

       A9: (g1 * (f opp )) = (g2 * (f opp ));

      ( Hom ((b opp ),a)) = ( Hom (( opp a),( opp (b opp )))) by Th5

      .= ( Hom (( opp a),b));

      then ( opp g1) in ( Hom (( opp a),b)) & ( opp g2) in ( Hom (( opp a),b)) by A8, CAT_1:def 5;

      then

      reconsider f1 = ( opp g1), f2 = ( opp g2) as Morphism of ( opp a), b by CAT_1:def 5;

      

       A10: ( Hom (( opp a),( opp (b opp )))) <> {} by A8, Th5;

      (f * f1) = ((f1 opp ) * (f opp )) by A6, Lm3, A10

      .= (g2 * (f opp )) by A9, Def6, A10

      .= ((f2 opp ) * (f opp )) by Def6, A10

      .= (f * f2) by A6, Lm3, A10;

      hence thesis by A7, A10;

    end;

    theorem :: OPPCAT_1:24

    for a,b be Object of C holds for f be Morphism of a, b holds (f opp ) is invertible iff f is invertible

    proof

      let a,b be Object of C;

      let f be Morphism of a, b;

      thus (f opp ) is invertible implies f is invertible

      proof

        assume

         A1: ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((a opp ),(b opp ))) <> {} ;

        given gg be Morphism of (a opp ), (b opp ) such that

         A2: ((f opp ) * gg) = ( id (a opp )) & (gg * (f opp )) = ( id (b opp ));

        thus

         A3: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A1, Th4;

        reconsider g = ( opp gg) as Morphism of b, a;

        take g;

        

         A4: (g opp ) = g by Def6, A3

        .= gg by Def7, A1;

        

        thus (f * g) = ((g opp ) * (f opp )) by A3, Lm3

        .= ( id (b opp )) by A2, A4

        .= ( id b) by Lm2;

        

        thus (g * f) = ((f opp ) * (g opp )) by A3, Lm3

        .= ( id a) by A2, A4, Lm2;

      end;

      assume

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

      given g be Morphism of b, a such that

       A6: (f * g) = ( id b) & (g * f) = ( id a);

      thus ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((a opp ),(b opp ))) <> {} by A5, Th4;

      take (g opp );

      

      thus ((f opp ) * (g opp )) = (g * f) by A5, Lm3

      .= ( id (a opp )) by A6, Lm2;

      

      thus ((g opp ) * (f opp )) = (f * g) by A5, Lm3

      .= ( id (b opp )) by A6, Lm2;

    end;

    theorem :: OPPCAT_1:25

    for c be Object of C holds c is initial iff (c opp ) is terminal

    proof

      let c be Object of C;

      thus c is initial implies (c opp ) is terminal

      proof

        assume

         A1: c is initial;

        let b be Object of (C opp );

        consider f be Morphism of c, ( opp b) such that

         A2: for g be Morphism of c, ( opp b) holds f = g by A1;

        

         A3: (( opp b) opp ) = b;

        

         A4: ( Hom (c,( opp b))) <> {} by A1;

        reconsider f9 = (f opp ) as Morphism of b, (c opp );

        thus

         A5: ( Hom (b,(c opp ))) <> {} by A3, Th4, A4;

        take f9;

        let g be Morphism of b, (c opp );

        ( opp (c opp )) = c;

        then ( opp g) is Morphism of c, ( opp b) by A5, Th13;

        

        hence g = f by A2

        .= f9 by A4, Def6;

      end;

      assume

       A6: (c opp ) is terminal;

      let b be Object of C;

      consider f be Morphism of (b opp ), (c opp ) such that

       A7: for g be Morphism of (b opp ), (c opp ) holds f = g by A6;

      

       A8: ( opp (c opp )) = c & ( opp (b opp )) = b;

      

       A9: ( Hom ((b opp ),(c opp ))) <> {} by A6;

      reconsider f9 = ( opp f) as Morphism of c, b;

      thus

       A10: ( Hom (c,b)) <> {} by A8, Th5, A9;

      take f9;

      let g be Morphism of c, b;

      (g opp ) = f by A7;

      

      hence g = f by Def6, A10

      .= f9 by A9, Def7;

    end;

    theorem :: OPPCAT_1:26

    for c be Object of C holds (c opp ) is initial iff c is terminal

    proof

      let c be Object of C;

      thus (c opp ) is initial implies c is terminal

      proof

        assume

         A1: (c opp ) is initial;

        let b be Object of C;

        consider f be Morphism of (c opp ), (b opp ) such that

         A2: for g be Morphism of (c opp ), (b opp ) holds f = g by A1;

        

         A3: ( opp (b opp )) = b & ( opp (c opp )) = c;

        

         A4: ( Hom ((c opp ),(b opp ))) <> {} by A1;

        reconsider f9 = ( opp f) as Morphism of b, c;

        thus

         A5: ( Hom (b,c)) <> {} by A3, Th5, A4;

        take f9;

        let g be Morphism of b, c;

        (g opp ) = f by A2;

        

        hence g = f by A5, Def6

        .= f9 by Def7, A4;

      end;

      assume

       A6: c is terminal;

      let b be Object of (C opp );

      consider f be Morphism of ( opp b), c such that

       A7: for g be Morphism of ( opp b), c holds f = g by A6;

      

       A8: (( opp b) opp ) = b;

      

       A9: ( Hom (( opp b),c)) <> {} by A6;

      reconsider f9 = (f opp ) as Morphism of (c opp ), b;

      thus

       A10: ( Hom ((c opp ),b)) <> {} by A8, Th4, A9;

      take f9;

      let g be Morphism of (c opp ), b;

      ( opp g) is Morphism of ( opp b), ( opp (c opp )) by A10, Th13;

      

      hence g = f by A7

      .= f9 by Def6, A9;

    end;

    definition

      let C, B;

      let S be Function of the carrier' of (C opp ), the carrier' of B;

      :: OPPCAT_1:def8

      func /* S -> Function of the carrier' of C, the carrier' of B means

      : Def8: for f be Morphism of C holds (it . f) = (S . (f opp ));

      existence

      proof

        deffunc F( Morphism of C) = (S . ($1 opp ));

        thus ex F be Function of the carrier' of C, the carrier' of B st for f be Morphism of C holds (F . f) = F(f) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let T1,T2 be Function of the carrier' of C, the carrier' of B such that

         A1: for f be Morphism of C holds (T1 . f) = (S . (f opp )) and

         A2: for f be Morphism of C holds (T2 . f) = (S . (f opp ));

        now

          let f be Morphism of C;

          

          thus (T1 . f) = (S . (f opp )) by A1

          .= (T2 . f) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: OPPCAT_1:27

    for S be Function of the carrier' of (C opp ), the carrier' of B holds for f be Morphism of (C opp ) holds (( /* S) . ( opp f)) = (S . f)

    proof

      let S be Function of the carrier' of (C opp ), the carrier' of B;

      let f be Morphism of (C opp );

      

      thus (( /* S) . ( opp f)) = (S . (( opp f) opp )) by Def8

      .= (S . f);

    end;

    

     Lm4: for S be Functor of (C opp ), B, c be Object of C holds (( /* S) . ( id c)) = ( id (( Obj S) . (c opp )))

    proof

      let S be Functor of (C opp ), B, c be Object of C;

      reconsider i = ( id c) as Morphism of C;

      

       A1: ( Hom (c,c)) <> {} ;

      

      thus (( /* S) . ( id c)) = (S . (i opp )) by Def8

      .= (S . (( id c) opp )) by A1, Def6

      .= (S . ( id (c opp ))) by Th18

      .= ( id (( Obj S) . (c opp ))) by CAT_1: 68;

    end;

    theorem :: OPPCAT_1:28

    

     Th26: for S be Functor of (C opp ), B, c be Object of C holds (( Obj ( /* S)) . c) = (( Obj S) . (c opp ))

    proof

      let S be Functor of (C opp ), B, c be Object of C;

       A1:

      now

        let c be Object of C;

        (( /* S) . ( id c)) = ( id (( Obj S) . (c opp ))) by Lm4;

        hence ex d be Object of B st (( /* S) . ( id c)) = ( id d);

      end;

      (( /* S) . ( id c)) = ( id (( Obj S) . (c opp ))) by Lm4;

      hence thesis by A1, CAT_1: 66;

    end;

    theorem :: OPPCAT_1:29

    for S be Functor of (C opp ), B, c be Object of (C opp ) holds (( Obj ( /* S)) . ( opp c)) = (( Obj S) . c)

    proof

      let S be Functor of (C opp ), B, c be Object of (C opp );

      

      thus (( Obj ( /* S)) . ( opp c)) = (( Obj S) . (( opp c) opp )) by Th26

      .= (( Obj S) . c);

    end;

    

     Lm5: for S be Functor of (C opp ), B, c be Object of C holds (( /* S) . ( id c)) = ( id (( Obj ( /* S)) . c))

    proof

      let S be Functor of (C opp ), B, c be Object of C;

      reconsider i = ( id c) as Morphism of C;

      

       A1: ( Hom (c,c)) <> {} ;

      

      thus (( /* S) . ( id c)) = (S . (i opp )) by Def8

      .= (S . (( id c) opp )) by Def6, A1

      .= (S . ( id (c opp ))) by Th18

      .= ( id (( Obj S) . (c opp ))) by CAT_1: 68

      .= ( id (( Obj ( /* S)) . c)) by Th26;

    end;

     Lm6:

    now

      let C, B;

      let S be Functor of (C opp ), B, c be Object of C;

      (( /* S) . ( id c)) = ( id (( Obj ( /* S)) . c)) by Lm5;

      hence ex d be Object of B st (( /* S) . ( id c)) = ( id d);

    end;

    

     Lm7: for S be Functor of (C opp ), B, f be Morphism of C holds (( Obj ( /* S)) . ( dom f)) = ( cod (( /* S) . f)) & (( Obj ( /* S)) . ( cod f)) = ( dom (( /* S) . f))

    proof

      let S be Functor of (C opp ), B, f be Morphism of C;

      

       A1: (( Obj ( /* S)) . ( cod f)) = (( Obj S) . (( cod f) opp )) by Th26

      .= (( Obj S) . ( dom (f opp )))

      .= ( dom (S . (f opp ))) by CAT_1: 69;

      (( Obj ( /* S)) . ( dom f)) = (( Obj S) . (( dom f) opp )) by Th26

      .= (( Obj S) . ( cod (f opp )))

      .= ( cod (S . (f opp ))) by CAT_1: 69;

      hence thesis by A1, Def8;

    end;

     Lm8:

    now

      let C, B;

      let S be Functor of (C opp ), B, f be Morphism of C;

      

      thus (( /* S) . ( id ( dom f))) = ( id (( Obj ( /* S)) . ( dom f))) by Lm5

      .= ( id ( cod (( /* S) . f))) by Lm7;

      

      thus (( /* S) . ( id ( cod f))) = ( id (( Obj ( /* S)) . ( cod f))) by Lm5

      .= ( id ( dom (( /* S) . f))) by Lm7;

    end;

    

     Lm9: for S be Functor of (C opp ), B holds for a,b,c be Object of C st ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds (( /* S) . (g (*) f)) = ((( /* S) . f) (*) (( /* S) . g))

    proof

      let S be Functor of (C opp ), B;

      let a,b,c be Object of C such that

       A1: ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} ;

      

       A2: ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((c opp ),(b opp ))) <> {} by A1, Th4;

      let f be Morphism of a, b, g be Morphism of b, c;

      

       A3: ( dom g) = b by A1, CAT_1: 5

      .= ( cod f) by A1, CAT_1: 5;

      

       A4: ( dom (f opp )) = (b opp ) by A2, CAT_1: 5

      .= ( cod f) by A1, CAT_1: 5;

      

       A5: ( cod (g opp )) = (b opp ) by A2, CAT_1: 5

      .= ( dom g) by A1, CAT_1: 5;

      

       A6: (S . (f opp )) = (S . (f qua Morphism of C opp )) by A1, Def6

      .= (( /* S) . f) by Def8;

      

       A7: (S . (g opp )) = (S . (g qua Morphism of C opp )) by A1, Def6

      .= (( /* S) . g) by Def8;

      

      thus (( /* S) . (g (*) f)) = (S . ((g (*) f) opp )) by Def8

      .= (S . ((f opp ) (*) (g opp ))) by Th14, A1

      .= ((( /* S) . f) (*) (( /* S) . g)) by A7, A6, A5, A3, A4, CAT_1: 64;

    end;

    definition

      let C, D;

      :: OPPCAT_1:def9

      mode Contravariant_Functor of C,D -> Function of the carrier' of C, the carrier' of D means

      : Def9: (for c be Object of C holds ex d be Object of D st (it . ( id c)) = ( id d)) & (for f be Morphism of C holds (it . ( id ( dom f))) = ( id ( cod (it . f))) & (it . ( id ( cod f))) = ( id ( dom (it . f)))) & for f,g be Morphism of C st ( dom g) = ( cod f) holds (it . (g (*) f)) = ((it . f) (*) (it . g));

      existence

      proof

        set S = the Functor of (C opp ), D;

        take ( /* S);

        thus for c be Object of C holds ex d be Object of D st (( /* S) . ( id c)) = ( id d) by Lm6;

        thus for f be Morphism of C holds (( /* S) . ( id ( dom f))) = ( id ( cod (( /* S) . f))) & (( /* S) . ( id ( cod f))) = ( id ( dom (( /* S) . f))) by Lm8;

        let f,g be Morphism of C such that

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

        reconsider ff = f as Morphism of ( dom f), ( cod f) by CAT_1: 4;

        reconsider gg = g as Morphism of ( cod f), ( cod g) by A1, CAT_1: 4;

        ( Hom (( dom f),( cod f))) <> {} & ( Hom (( dom g),( cod g))) <> {} by CAT_1: 2;

        then (( /* S) . (gg (*) ff)) = ((( /* S) . ff) (*) (( /* S) . gg)) by A1, Lm9;

        hence thesis;

      end;

    end

    theorem :: OPPCAT_1:30

    

     Th28: for S be Contravariant_Functor of C, D, c be Object of C, d be Object of D st (S . ( id c)) = ( id d) holds (( Obj S) . c) = d

    proof

      let S be Contravariant_Functor of C, D;

      let c be Object of C, d be Object of D;

      for c be Object of C holds ex d be Object of D st (S . ( id c)) = ( id d) by Def9;

      hence thesis by CAT_1: 66;

    end;

    theorem :: OPPCAT_1:31

    

     Th29: for S be Contravariant_Functor of C, D, c be Object of C holds (S . ( id c)) = ( id (( Obj S) . c))

    proof

      let S be Contravariant_Functor of C, D, c be Object of C;

      ex d be Object of D st (S . ( id c)) = ( id d) by Def9;

      hence thesis by Th28;

    end;

    theorem :: OPPCAT_1:32

    

     Th30: for S be Contravariant_Functor of C, D, f be Morphism of C holds (( Obj S) . ( dom f)) = ( cod (S . f)) & (( Obj S) . ( cod f)) = ( dom (S . f))

    proof

      let S be Contravariant_Functor of C, D, f be Morphism of C;

      (S . ( id ( dom f))) = ( id ( cod (S . f))) & (S . ( id ( cod f))) = ( id ( dom (S . f))) by Def9;

      hence thesis by Th28;

    end;

    theorem :: OPPCAT_1:33

    

     Th31: for S be Contravariant_Functor of C, D, f,g be Morphism of C st ( dom g) = ( cod f) holds ( dom (S . f)) = ( cod (S . g))

    proof

      let S be Contravariant_Functor of C, D, f,g be Morphism of C;

      assume ( dom g) = ( cod f);

      

      hence ( dom (S . f)) = (( Obj S) . ( dom g)) by Th30

      .= ( cod (S . g)) by Th30;

    end;

    theorem :: OPPCAT_1:34

    

     Th32: for S be Functor of (C opp ), B holds ( /* S) is Contravariant_Functor of C, B

    proof

      let S be Functor of (C opp ), B;

      thus for c be Object of C holds ex d be Object of B st (( /* S) . ( id c)) = ( id d) by Lm6;

      thus for f be Morphism of C holds (( /* S) . ( id ( dom f))) = ( id ( cod (( /* S) . f))) & (( /* S) . ( id ( cod f))) = ( id ( dom (( /* S) . f))) by Lm8;

      let f,g be Morphism of C such that

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

      reconsider ff = f as Morphism of ( dom f), ( cod f) by CAT_1: 4;

      reconsider gg = g as Morphism of ( cod f), ( cod g) by A1, CAT_1: 4;

      ( Hom (( dom f),( cod f))) <> {} & ( Hom (( dom g),( cod g))) <> {} by CAT_1: 2;

      then (( /* S) . (gg (*) ff)) = ((( /* S) . ff) (*) (( /* S) . gg)) by A1, Lm9;

      hence thesis;

    end;

    theorem :: OPPCAT_1:35

    

     Th33: for S1 be Contravariant_Functor of C, B, S2 be Contravariant_Functor of B, D holds (S2 * S1) is Functor of C, D

    proof

      let S1 be Contravariant_Functor of C, B, S2 be Contravariant_Functor of B, D;

      set T = (S2 * S1);

      now

        thus for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d)

        proof

          let c be Object of C;

          consider b be Object of B such that

           A1: (S1 . ( id c)) = ( id b) by Def9;

          consider d be Object of D such that

           A2: (S2 . ( id b)) = ( id d) by Def9;

          take d;

          thus thesis by A1, A2, FUNCT_2: 15;

        end;

        thus for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))

        proof

          let f be Morphism of C;

          

          thus (T . ( id ( dom f))) = (S2 . (S1 . ( id ( dom f)))) by FUNCT_2: 15

          .= (S2 . ( id ( cod (S1 . f)))) by Def9

          .= ( id ( dom (S2 . (S1 . f)))) by Def9

          .= ( id ( dom (T . f))) by FUNCT_2: 15;

          

          thus (T . ( id ( cod f))) = (S2 . (S1 . ( id ( cod f)))) by FUNCT_2: 15

          .= (S2 . ( id ( dom (S1 . f)))) by Def9

          .= ( id ( cod (S2 . (S1 . f)))) by Def9

          .= ( id ( cod (T . f))) by FUNCT_2: 15;

        end;

        let f,g be Morphism of C;

        assume

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

        then

         A4: ( cod (S1 . g)) = ( dom (S1 . f)) by Th31;

        

        thus (T . (g (*) f)) = (S2 . (S1 . (g (*) f))) by FUNCT_2: 15

        .= (S2 . ((S1 . f) (*) (S1 . g))) by A3, Def9

        .= ((S2 . (S1 . g)) (*) (S2 . (S1 . f))) by A4, Def9

        .= ((T . g) (*) (S2 . (S1 . f))) by FUNCT_2: 15

        .= ((T . g) (*) (T . f)) by FUNCT_2: 15;

      end;

      hence thesis by CAT_1: 61;

    end;

    

     Lm10: for S be Contravariant_Functor of (C opp ), B, c be Object of C holds (( /* S) . ( id c)) = ( id (( Obj S) . (c opp )))

    proof

      let S be Contravariant_Functor of (C opp ), B, c be Object of C;

      reconsider i = ( id c) as Morphism of C;

      

       A1: ( Hom (c,c)) <> {} ;

      

      thus (( /* S) . ( id c)) = (S . (i opp )) by Def8

      .= (S . (( id c) opp )) by Def6, A1

      .= (S . ( id (c opp ))) by Th18

      .= ( id (( Obj S) . (c opp ))) by Th29;

    end;

    theorem :: OPPCAT_1:36

    

     Th34: for S be Contravariant_Functor of (C opp ), B, c be Object of C holds (( Obj ( /* S)) . c) = (( Obj S) . (c opp ))

    proof

      let S be Contravariant_Functor of (C opp ), B, c be Object of C;

       A1:

      now

        let c be Object of C;

        (( /* S) . ( id c)) = ( id (( Obj S) . (c opp ))) by Lm10;

        hence ex d be Object of B st (( /* S) . ( id c)) = ( id d);

      end;

      (( /* S) . ( id c)) = ( id (( Obj S) . (c opp ))) by Lm10;

      hence thesis by A1, CAT_1: 66;

    end;

    theorem :: OPPCAT_1:37

    for S be Contravariant_Functor of (C opp ), B, c be Object of (C opp ) holds (( Obj ( /* S)) . ( opp c)) = (( Obj S) . c)

    proof

      let S be Contravariant_Functor of (C opp ), B, c be Object of (C opp );

      

      thus (( Obj ( /* S)) . ( opp c)) = (( Obj S) . (( opp c) opp )) by Th34

      .= (( Obj S) . c);

    end;

    

     Lm11: for S be Contravariant_Functor of (C opp ), B, c be Object of C holds (( /* S) . ( id c)) = ( id (( Obj ( /* S)) . c))

    proof

      let S be Contravariant_Functor of (C opp ), B, c be Object of C;

      reconsider i = ( id c) as Morphism of C;

      

       A1: ( Hom (c,c)) <> {} ;

      

      thus (( /* S) . ( id c)) = (S . (i opp )) by Def8

      .= (S . (( id c) opp )) by Def6, A1

      .= (S . ( id (c opp ))) by Th18

      .= ( id (( Obj S) . (c opp ))) by Th29

      .= ( id (( Obj ( /* S)) . c)) by Th34;

    end;

    

     Lm12: for S be Contravariant_Functor of (C opp ), B, f be Morphism of C holds (( Obj ( /* S)) . ( dom f)) = ( dom (( /* S) . f)) & (( Obj ( /* S)) . ( cod f)) = ( cod (( /* S) . f))

    proof

      let S be Contravariant_Functor of (C opp ), B, f be Morphism of C;

      

       A1: (( Obj ( /* S)) . ( cod f)) = (( Obj S) . (( cod f) opp )) by Th34

      .= (( Obj S) . ( dom (f opp )))

      .= ( cod (S . (f opp ))) by Th30;

      (( Obj ( /* S)) . ( dom f)) = (( Obj S) . (( dom f) opp )) by Th34

      .= (( Obj S) . ( cod (f opp )))

      .= ( dom (S . (f opp ))) by Th30;

      hence thesis by A1, Def8;

    end;

    theorem :: OPPCAT_1:38

    for S be Contravariant_Functor of (C opp ), B holds ( /* S) is Functor of C, B

    proof

      let S be Contravariant_Functor of (C opp ), B;

      now

        thus for c be Object of C holds ex d be Object of B st (( /* S) . ( id c)) = ( id d)

        proof

          let c be Object of C;

          (( /* S) . ( id c)) = ( id (( Obj ( /* S)) . c)) by Lm11;

          hence thesis;

        end;

        thus for f be Morphism of C holds (( /* S) . ( id ( dom f))) = ( id ( dom (( /* S) . f))) & (( /* S) . ( id ( cod f))) = ( id ( cod (( /* S) . f)))

        proof

          let f be Morphism of C;

          

          thus (( /* S) . ( id ( dom f))) = ( id (( Obj ( /* S)) . ( dom f))) by Lm11

          .= ( id ( dom (( /* S) . f))) by Lm12;

          

          thus (( /* S) . ( id ( cod f))) = ( id (( Obj ( /* S)) . ( cod f))) by Lm11

          .= ( id ( cod (( /* S) . f))) by Lm12;

        end;

        let f,g be Morphism of C such that

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

        

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

        reconsider ff = f as Morphism of ( dom f), ( cod f) by CAT_1: 4;

        reconsider gg = g as Morphism of ( cod f), ( cod g) by A1, CAT_1: 4;

        

         A3: ( Hom (( dom f),( cod f))) <> {} & ( Hom (( dom g),( cod g))) <> {} by CAT_1: 2;

        then

         A4: (ff opp ) = (f opp ) by Def6;

        

         A5: (gg opp ) = (g opp ) by Def6, A3, A1;

        

        thus (( /* S) . (g (*) f)) = (S . ((g (*) f) opp )) by Def8

        .= (S . ((f opp ) (*) (g opp ))) by A4, A5, A3, A1, Th14

        .= ((S . (g opp )) (*) (S . (f opp ))) by A1, A2, Def9

        .= ((( /* S) . g) (*) (S . (f opp ))) by Def8

        .= ((( /* S) . g) (*) (( /* S) . f)) by Def8;

      end;

      hence thesis by CAT_1: 61;

    end;

    definition

      let C, B;

      let S be Function of the carrier' of C, the carrier' of B;

      :: OPPCAT_1:def10

      func *' S -> Function of the carrier' of (C opp ), the carrier' of B means

      : Def10: for f be Morphism of (C opp ) holds (it . f) = (S . ( opp f));

      existence

      proof

        deffunc F( Morphism of (C opp )) = (S . ( opp $1));

        thus ex F be Function of the carrier' of (C opp ), the carrier' of B st for f be Morphism of (C opp ) holds (F . f) = F(f) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let T1,T2 be Function of the carrier' of (C opp ), the carrier' of B such that

         A1: for f be Morphism of (C opp ) holds (T1 . f) = (S . ( opp f)) and

         A2: for f be Morphism of (C opp ) holds (T2 . f) = (S . ( opp f));

        now

          let f be Morphism of (C opp );

          

          thus (T1 . f) = (S . ( opp f)) by A1

          .= (T2 . f) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: OPPCAT_1:def11

      func S *' -> Function of the carrier' of C, the carrier' of (B opp ) means

      : Def11: for f be Morphism of C holds (it . f) = ((S . f) opp );

      existence

      proof

        deffunc F( Morphism of C) = ((S . $1) opp );

        thus ex F be Function of the carrier' of C, the carrier' of (B opp ) st for f be Morphism of C holds (F . f) = F(f) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let T1,T2 be Function of the carrier' of C, the carrier' of (B opp ) such that

         A3: for f be Morphism of C holds (T1 . f) = ((S . f) opp ) and

         A4: for f be Morphism of C holds (T2 . f) = ((S . f) opp );

        now

          let f be Morphism of C;

          

          thus (T1 . f) = ((S . f) opp ) by A3

          .= (T2 . f) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: OPPCAT_1:39

    for S be Function of the carrier' of C, the carrier' of B holds for f be Morphism of C holds (( *' S) . (f opp )) = (S . f)

    proof

      let S be Function of the carrier' of C, the carrier' of B;

      let f be Morphism of C;

      

      thus (( *' S) . (f opp )) = (S . ( opp (f opp ))) by Def10

      .= (S . f);

    end;

    

     Lm13: for S be Functor of C, B, c be Object of (C opp ) holds (( *' S) . ( id c)) = ( id (( Obj S) . ( opp c)))

    proof

      let S be Functor of C, B, c be Object of (C opp );

      

      thus (( *' S) . ( id c)) = (S . ( opp ( id c))) by Def10

      .= (S . ( id ( opp c))) by Th19

      .= ( id (( Obj S) . ( opp c))) by CAT_1: 68;

    end;

    theorem :: OPPCAT_1:40

    

     Th38: for S be Functor of C, B, c be Object of (C opp ) holds (( Obj ( *' S)) . c) = (( Obj S) . ( opp c))

    proof

      let S be Functor of C, B, c be Object of (C opp );

      now

        thus (( *' S) . ( id c)) = ( id (( Obj S) . ( opp c))) by Lm13;

        let c be Object of (C opp );

        (( *' S) . ( id c)) = ( id (( Obj S) . ( opp c))) by Lm13;

        hence ex d be Object of B st (( *' S) . ( id c)) = ( id d);

      end;

      hence thesis by CAT_1: 66;

    end;

    theorem :: OPPCAT_1:41

    for S be Functor of C, B, c be Object of C holds (( Obj ( *' S)) . (c opp )) = (( Obj S) . c)

    proof

      let S be Functor of C, B, c be Object of C;

      

      thus (( Obj ( *' S)) . (c opp )) = (( Obj S) . ( opp (c opp ))) by Th38

      .= (( Obj S) . c);

    end;

    

     Lm14: for S be Functor of C, B, c be Object of C holds ((S *' ) . ( id c)) = ( id ((( Obj S) . c) opp ))

    proof

      let S be Functor of C, B, c be Object of C;

      

       A1: ( Hom ((( Obj S) . c),(( Obj S) . c))) <> {} ;

      

      thus ((S *' ) . ( id c)) = ((S . ( id c)) opp ) by Def11

      .= (( id (( Obj S) . c)) qua Morphism of B opp ) by CAT_1: 68

      .= (( id (( Obj S) . c)) opp ) by Def6, A1

      .= ( id ((( Obj S) . c) opp )) by Th18;

    end;

    theorem :: OPPCAT_1:42

    

     Th40: for S be Functor of C, B, c be Object of C holds (( Obj (S *' )) . c) = ((( Obj S) . c) opp )

    proof

      let S be Functor of C, B, c be Object of C;

      now

        thus ((S *' ) . ( id c)) = ( id ((( Obj S) . c) opp )) by Lm14;

        let c be Object of C;

        ((S *' ) . ( id c)) = ( id ((( Obj S) . c) opp )) by Lm14;

        hence ex d be Object of (B opp ) st ((S *' ) . ( id c)) = ( id d);

      end;

      hence thesis by CAT_1: 66;

    end;

    

     Lm15: for S be Contravariant_Functor of C, B, c be Object of (C opp ) holds (( *' S) . ( id c)) = ( id (( Obj S) . ( opp c)))

    proof

      let S be Contravariant_Functor of C, B, c be Object of (C opp );

      

      thus (( *' S) . ( id c)) = (S . ( opp ( id c))) by Def10

      .= (S . ( id ( opp c))) by Th19

      .= ( id (( Obj S) . ( opp c))) by Th29;

    end;

    theorem :: OPPCAT_1:43

    

     Th41: for S be Contravariant_Functor of C, B, c be Object of (C opp ) holds (( Obj ( *' S)) . c) = (( Obj S) . ( opp c))

    proof

      let S be Contravariant_Functor of C, B, c be Object of (C opp );

      now

        thus (( *' S) . ( id c)) = ( id (( Obj S) . ( opp c))) by Lm15;

        let c be Object of (C opp );

        (( *' S) . ( id c)) = ( id (( Obj S) . ( opp c))) by Lm15;

        hence ex d be Object of B st (( *' S) . ( id c)) = ( id d);

      end;

      hence thesis by CAT_1: 66;

    end;

    theorem :: OPPCAT_1:44

    for S be Contravariant_Functor of C, B, c be Object of C holds (( Obj ( *' S)) . (c opp )) = (( Obj S) . c)

    proof

      let S be Contravariant_Functor of C, B, c be Object of C;

      

      thus (( Obj ( *' S)) . (c opp )) = (( Obj S) . ( opp (c opp ))) by Th41

      .= (( Obj S) . c);

    end;

    

     Lm16: for S be Contravariant_Functor of C, B, c be Object of C holds ((S *' ) . ( id c)) = ( id ((( Obj S) . c) opp ))

    proof

      let S be Contravariant_Functor of C, B, c be Object of C;

      

       A1: ( Hom ((( Obj S) . c),(( Obj S) . c))) <> {} ;

      

      thus ((S *' ) . ( id c)) = ((S . ( id c)) opp ) by Def11

      .= (( id (( Obj S) . c)) qua Morphism of B opp ) by Th29

      .= (( id (( Obj S) . c)) opp ) by Def6, A1

      .= ( id ((( Obj S) . c) opp )) by Th18;

    end;

    theorem :: OPPCAT_1:45

    

     Th43: for S be Contravariant_Functor of C, B, c be Object of C holds (( Obj (S *' )) . c) = ((( Obj S) . c) opp )

    proof

      let S be Contravariant_Functor of C, B, c be Object of C;

      now

        thus ((S *' ) . ( id c)) = ( id ((( Obj S) . c) opp )) by Lm16;

        let c be Object of C;

        ((S *' ) . ( id c)) = ( id ((( Obj S) . c) opp )) by Lm16;

        hence ex d be Object of (B opp ) st ((S *' ) . ( id c)) = ( id d);

      end;

      hence thesis by CAT_1: 66;

    end;

    

     Lm17: for F be Function of the carrier' of C, the carrier' of D holds for f be Morphism of (C opp ) holds ((( *' F) *' ) . f) = ((F . ( opp f)) opp )

    proof

      let F be Function of the carrier' of C, the carrier' of D;

      let f be Morphism of (C opp );

      

      thus ((( *' F) *' ) . f) = ((( *' F) . f) opp ) by Def11

      .= ((F . ( opp f)) opp ) by Def10;

    end;

    theorem :: OPPCAT_1:46

    

     Th44: for F be Function of the carrier' of C, the carrier' of D holds for f be Morphism of C holds ((( *' F) *' ) . (f opp )) = ((F . f) opp )

    proof

      let F be Function of the carrier' of C, the carrier' of D;

      let f be Morphism of C;

      

      thus ((( *' F) *' ) . (f opp )) = ((F . ( opp (f opp ))) opp ) by Lm17

      .= ((F . f) opp );

    end;

    theorem :: OPPCAT_1:47

    

     Th45: for S be Function of the carrier' of C, the carrier' of D holds ( /* ( *' S)) = S

    proof

      let S be Function of the carrier' of C, the carrier' of D;

      now

        let f be Morphism of C;

        

        thus (( /* ( *' S)) . f) = (( *' S) . (f opp )) by Def8

        .= (S . ( opp (f opp ))) by Def10

        .= (S . f);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:48

    for S be Function of the carrier' of (C opp ), the carrier' of D holds ( *' ( /* S)) = S

    proof

      let S be Function of the carrier' of (C opp ), the carrier' of D;

      now

        let f be Morphism of (C opp );

        

        thus (( *' ( /* S)) . f) = (( /* S) . ( opp f)) by Def10

        .= (S . (( opp f) opp )) by Def8

        .= (S . f);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:49

    for S be Function of the carrier' of C, the carrier' of D holds (( *' S) *' ) = ( *' (S *' ))

    proof

      let S be Function of the carrier' of C, the carrier' of D;

      now

        let f be Morphism of (C opp );

        

        thus ((( *' S) *' ) . f) = ((( *' S) . f) opp ) by Def11

        .= ((S . ( opp f)) opp ) by Def10

        .= ((S *' ) . ( opp f)) by Def11

        .= (( *' (S *' )) . f) by Def10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:50

    for D be strict Category, S be Function of the carrier' of C, the carrier' of D holds ((S *' ) *' ) = S

    proof

      let D be strict Category;

      let S be Function of the carrier' of C, the carrier' of D;

      now

        thus ((D opp ) opp ) = D by FUNCT_4: 53;

        let f be Morphism of C;

        

        thus (((S *' ) *' ) . f) = (((S *' ) . f) opp ) by Def11

        .= (((S . f) opp ) opp ) by Def11

        .= (S . f);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:51

    for C be strict Category, S be Function of the carrier' of C, the carrier' of D holds ( *' ( *' S)) = S

    proof

      let C be strict Category;

      let S be Function of the carrier' of C, the carrier' of D;

      now

        thus ((C opp ) opp ) = C by FUNCT_4: 53;

        let f be Morphism of ((C opp ) opp );

        

        thus (( *' ( *' S)) . f) = (( *' S) . ( opp f)) by Def10

        .= (S . ( opp ( opp f))) by Def10

        .= (S . f);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm18: for S be Function of the carrier' of (C opp ), the carrier' of B holds for T be Function of the carrier' of B, the carrier' of D holds ( /* (T * S)) = (T * ( /* S))

    proof

      let S be Function of the carrier' of (C opp ), the carrier' of B;

      let T be Function of the carrier' of B, the carrier' of D;

      now

        let f be Morphism of C;

        

        thus (( /* (T * S)) . f) = ((T * S) . (f opp )) by Def8

        .= (T . (S . (f opp ))) by FUNCT_2: 15

        .= (T . (( /* S) . f)) by Def8

        .= ((T * ( /* S)) . f) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:52

    for S be Function of the carrier' of C, the carrier' of B holds for T be Function of the carrier' of B, the carrier' of D holds ( *' (T * S)) = (T * ( *' S))

    proof

      let S be Function of the carrier' of C, the carrier' of B;

      let T be Function of the carrier' of B, the carrier' of D;

      now

        let f be Morphism of (C opp );

        

        thus (( *' (T * S)) . f) = ((T * S) . ( opp f)) by Def10

        .= (T . (S . ( opp f))) by FUNCT_2: 15

        .= (T . (( *' S) . f)) by Def10

        .= ((T * ( *' S)) . f) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:53

    for S be Function of the carrier' of C, the carrier' of B holds for T be Function of the carrier' of B, the carrier' of D holds ((T * S) *' ) = ((T *' ) * S)

    proof

      let S be Function of the carrier' of C, the carrier' of B;

      let T be Function of the carrier' of B, the carrier' of D;

      now

        let f be Morphism of C;

        

        thus (((T * S) *' ) . f) = (((T * S) . f) opp ) by Def11

        .= ((T . (S . f)) opp ) by FUNCT_2: 15

        .= ((T *' ) . (S . f)) by Def11

        .= (((T *' ) * S) . f) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:54

    for F1 be Function of the carrier' of C, the carrier' of B holds for F2 be Function of the carrier' of B, the carrier' of D holds (( *' (F2 * F1)) *' ) = ((( *' F2) *' ) * (( *' F1) *' ))

    proof

      let F1 be Function of the carrier' of C, the carrier' of B;

      let F2 be Function of the carrier' of B, the carrier' of D;

      now

        let f be Morphism of (C opp );

        

        thus ((( *' (F2 * F1)) *' ) . f) = (((F2 * F1) . ( opp f)) opp ) by Lm17

        .= ((F2 . (F1 . ( opp f))) opp ) by FUNCT_2: 15

        .= ((( *' F2) *' ) . ((F1 . ( opp f)) opp )) by Th44

        .= ((( *' F2) *' ) . ((( *' F1) *' ) . f)) by Lm17

        .= (((( *' F2) *' ) * (( *' F1) *' )) . f) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm19: for S be Contravariant_Functor of C, B, c be Object of (C opp ) holds (( *' S) . ( id c)) = ( id (( Obj ( *' S)) . c))

    proof

      let S be Contravariant_Functor of C, B, c be Object of (C opp );

      

      thus (( *' S) . ( id c)) = (S . ( opp ( id c))) by Def10

      .= (S . ( id ( opp c))) by Th19

      .= ( id (( Obj S) . ( opp c))) by Th29

      .= ( id (( Obj ( *' S)) . c)) by Th41;

    end;

    

     Lm20: for S be Contravariant_Functor of C, B, f be Morphism of (C opp ) holds (( Obj ( *' S)) . ( dom f)) = ( dom (( *' S) . f)) & (( Obj ( *' S)) . ( cod f)) = ( cod (( *' S) . f))

    proof

      let S be Contravariant_Functor of C, B, f be Morphism of (C opp );

      

       A1: (( Obj ( *' S)) . ( cod f)) = (( Obj S) . ( opp ( cod f))) by Th41

      .= (( Obj S) . ( dom ( opp f)))

      .= ( cod (S . ( opp f))) by Th30;

      (( Obj ( *' S)) . ( dom f)) = (( Obj S) . ( opp ( dom f))) by Th41

      .= (( Obj S) . ( cod ( opp f)))

      .= ( dom (S . ( opp f))) by Th30;

      hence thesis by A1, Def10;

    end;

    theorem :: OPPCAT_1:55

    

     Th53: for S be Contravariant_Functor of C, D holds ( *' S) is Functor of (C opp ), D

    proof

      let S be Contravariant_Functor of C, D;

      now

        thus for c be Object of (C opp ) holds ex d be Object of D st (( *' S) . ( id c)) = ( id d)

        proof

          let c be Object of (C opp );

          (( *' S) . ( id c)) = ( id (( Obj ( *' S)) . c)) by Lm19;

          hence thesis;

        end;

        thus for f be Morphism of (C opp ) holds (( *' S) . ( id ( dom f))) = ( id ( dom (( *' S) . f))) & (( *' S) . ( id ( cod f))) = ( id ( cod (( *' S) . f)))

        proof

          let f be Morphism of (C opp );

          

          thus (( *' S) . ( id ( dom f))) = ( id (( Obj ( *' S)) . ( dom f))) by Lm19

          .= ( id ( dom (( *' S) . f))) by Lm20;

          

          thus (( *' S) . ( id ( cod f))) = ( id (( Obj ( *' S)) . ( cod f))) by Lm19

          .= ( id ( cod (( *' S) . f))) by Lm20;

        end;

        let f,g be Morphism of (C opp ) such that

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

        

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

        

        thus (( *' S) . (g (*) f)) = (S . ( opp (g (*) f))) by Def10

        .= (S . (( opp f) (*) ( opp g))) by A1, Th16

        .= ((S . ( opp g)) (*) (S . ( opp f))) by A1, A2, Def9

        .= ((( *' S) . g) (*) (S . ( opp f))) by Def10

        .= ((( *' S) . g) (*) (( *' S) . f)) by Def10;

      end;

      hence thesis by CAT_1: 61;

    end;

    

     Lm21: for S be Contravariant_Functor of C, B, c be Object of C holds ((S *' ) . ( id c)) = ( id (( Obj (S *' )) . c))

    proof

      let S be Contravariant_Functor of C, B, c be Object of C;

      

       A1: ( Hom ((( Obj S) . c),(( Obj S) . c))) <> {} ;

      

      thus ((S *' ) . ( id c)) = ((S . ( id c)) opp ) by Def11

      .= (( id (( Obj S) . c)) qua Morphism of B opp ) by Th29

      .= (( id (( Obj S) . c)) opp ) by Def6, A1

      .= ( id ((( Obj S) . c) opp )) by Th18

      .= ( id (( Obj (S *' )) . c)) by Th43;

    end;

    

     Lm22: for S be Contravariant_Functor of C, B, f be Morphism of C holds (( Obj (S *' )) . ( dom f)) = ( dom ((S *' ) . f)) & (( Obj (S *' )) . ( cod f)) = ( cod ((S *' ) . f))

    proof

      let S be Contravariant_Functor of C, B, f be Morphism of C;

      

       A1: (( Obj (S *' )) . ( cod f)) = ((( Obj S) . ( cod f)) opp ) by Th43

      .= (( dom (S . f)) opp ) by Th30

      .= ( cod ((S . f) opp ));

      (( Obj (S *' )) . ( dom f)) = ((( Obj S) . ( dom f)) opp ) by Th43

      .= (( cod (S . f)) opp ) by Th30

      .= ( dom ((S . f) opp ));

      hence thesis by A1, Def11;

    end;

    theorem :: OPPCAT_1:56

    

     Th54: for S be Contravariant_Functor of C, D holds (S *' ) is Functor of C, (D opp )

    proof

      let S be Contravariant_Functor of C, D;

      now

        thus for c be Object of C holds ex d be Object of (D opp ) st ((S *' ) . ( id c)) = ( id d)

        proof

          let c be Object of C;

          ((S *' ) . ( id c)) = ( id ((( Obj S) . c) opp )) by Lm16;

          hence thesis;

        end;

        thus for f be Morphism of C holds ((S *' ) . ( id ( dom f))) = ( id ( dom ((S *' ) . f))) & ((S *' ) . ( id ( cod f))) = ( id ( cod ((S *' ) . f)))

        proof

          let f be Morphism of C;

          

          thus ((S *' ) . ( id ( dom f))) = ( id (( Obj (S *' )) . ( dom f))) by Lm21

          .= ( id ( dom ((S *' ) . f))) by Lm22;

          

          thus ((S *' ) . ( id ( cod f))) = ( id (( Obj (S *' )) . ( cod f))) by Lm21

          .= ( id ( cod ((S *' ) . f))) by Lm22;

        end;

        let f,g be Morphism of C;

        assume

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

        then

         A2: ( dom (S . f)) = ( cod (S . g)) by Th31;

        reconsider Sff = (S . f) as Morphism of ( dom (S . f)), ( cod (S . f)) by CAT_1: 4;

        reconsider Sgg = (S . g) as Morphism of ( dom (S . g)), ( cod (S . g)) by CAT_1: 4;

        

         A3: ( Hom (( dom (S . f)),( cod (S . f)))) <> {} & ( Hom (( dom (S . g)),( cod (S . g)))) <> {} by CAT_1: 2;

        then

         A4: (Sff opp ) = ((S . f) opp ) by Def6;

        

         A5: (Sgg opp ) = ((S . g) opp ) by A3, Def6;

        

        thus ((S *' ) . (g (*) f)) = ((S . (g (*) f)) opp ) by Def11

        .= ((Sff (*) Sgg) opp ) by A1, Def9

        .= ((Sgg opp ) (*) (Sff opp )) by A3, A2, Th14

        .= (((S *' ) . g) (*) ((S . f) opp )) by Def11, A4, A5

        .= (((S *' ) . g) (*) ((S *' ) . f)) by Def11;

      end;

      hence thesis by CAT_1: 61;

    end;

    

     Lm23: for S be Functor of C, B, c be Object of (C opp ) holds (( *' S) . ( id c)) = ( id (( Obj ( *' S)) . c))

    proof

      let S be Functor of C, B, c be Object of (C opp );

      

      thus (( *' S) . ( id c)) = (S . ( opp ( id c))) by Def10

      .= (S . ( id ( opp c))) by Th19

      .= ( id (( Obj S) . ( opp c))) by CAT_1: 68

      .= ( id (( Obj ( *' S)) . c)) by Th38;

    end;

    

     Lm24: for S be Functor of C, B, f be Morphism of (C opp ) holds (( Obj ( *' S)) . ( dom f)) = ( cod (( *' S) . f)) & (( Obj ( *' S)) . ( cod f)) = ( dom (( *' S) . f))

    proof

      let S be Functor of C, B, f be Morphism of (C opp );

      

       A1: (( Obj ( *' S)) . ( cod f)) = (( Obj S) . ( opp ( cod f))) by Th38

      .= (( Obj S) . ( dom ( opp f)))

      .= ( dom (S . ( opp f))) by CAT_1: 69;

      (( Obj ( *' S)) . ( dom f)) = (( Obj S) . ( opp ( dom f))) by Th38

      .= (( Obj S) . ( cod ( opp f)))

      .= ( cod (S . ( opp f))) by CAT_1: 69;

      hence thesis by A1, Def10;

    end;

    theorem :: OPPCAT_1:57

    

     Th55: for S be Functor of C, D holds ( *' S) is Contravariant_Functor of (C opp ), D

    proof

      let S be Functor of C, D;

      thus for c be Object of (C opp ) holds ex d be Object of D st (( *' S) . ( id c)) = ( id d)

      proof

        let c be Object of (C opp );

        (( *' S) . ( id c)) = ( id (( Obj ( *' S)) . c)) by Lm23;

        hence thesis;

      end;

      thus for f be Morphism of (C opp ) holds (( *' S) . ( id ( dom f))) = ( id ( cod (( *' S) . f))) & (( *' S) . ( id ( cod f))) = ( id ( dom (( *' S) . f)))

      proof

        let f be Morphism of (C opp );

        

        thus (( *' S) . ( id ( dom f))) = ( id (( Obj ( *' S)) . ( dom f))) by Lm23

        .= ( id ( cod (( *' S) . f))) by Lm24;

        

        thus (( *' S) . ( id ( cod f))) = ( id (( Obj ( *' S)) . ( cod f))) by Lm23

        .= ( id ( dom (( *' S) . f))) by Lm24;

      end;

      let f,g be Morphism of (C opp ) such that

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

      

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

      

      thus (( *' S) . (g (*) f)) = (S . ( opp (g (*) f))) by Def10

      .= (S . (( opp f) (*) ( opp g))) by A1, Th16

      .= ((S . ( opp f)) (*) (S . ( opp g))) by A1, A2, CAT_1: 64

      .= ((( *' S) . f) (*) (S . ( opp g))) by Def10

      .= ((( *' S) . f) (*) (( *' S) . g)) by Def10;

    end;

    

     Lm25: for S be Functor of C, B, c be Object of C holds ((S *' ) . ( id c)) = ( id (( Obj (S *' )) . c))

    proof

      let S be Functor of C, B, c be Object of C;

      

       A1: ( Hom ((( Obj S) . c),(( Obj S) . c))) <> {} ;

      

      thus ((S *' ) . ( id c)) = ((S . ( id c)) opp ) by Def11

      .= (( id (( Obj S) . c)) qua Morphism of B opp ) by CAT_1: 68

      .= (( id (( Obj S) . c)) opp ) by Def6, A1

      .= ( id ((( Obj S) . c) opp )) by Th18

      .= ( id (( Obj (S *' )) . c)) by Th40;

    end;

    

     Lm26: for S be Functor of C, B, f be Morphism of C holds (( Obj (S *' )) . ( dom f)) = ( cod ((S *' ) . f)) & (( Obj (S *' )) . ( cod f)) = ( dom ((S *' ) . f))

    proof

      let S be Functor of C, B, f be Morphism of C;

      

       A1: (( Obj (S *' )) . ( cod f)) = ((( Obj S) . ( cod f)) opp ) by Th40

      .= (( cod (S . f)) opp ) by CAT_1: 69

      .= ( dom ((S . f) opp ));

      (( Obj (S *' )) . ( dom f)) = ((( Obj S) . ( dom f)) opp ) by Th40

      .= (( dom (S . f)) opp ) by CAT_1: 69

      .= ( cod ((S . f) opp ));

      hence thesis by A1, Def11;

    end;

    theorem :: OPPCAT_1:58

    

     Th56: for S be Functor of C, D holds (S *' ) is Contravariant_Functor of C, (D opp )

    proof

      let S be Functor of C, D;

      thus for c be Object of C holds ex d be Object of (D opp ) st ((S *' ) . ( id c)) = ( id d)

      proof

        let c be Object of C;

        ((S *' ) . ( id c)) = ( id (( Obj (S *' )) . c)) by Lm25;

        hence thesis;

      end;

      thus for f be Morphism of C holds ((S *' ) . ( id ( dom f))) = ( id ( cod ((S *' ) . f))) & ((S *' ) . ( id ( cod f))) = ( id ( dom ((S *' ) . f)))

      proof

        let f be Morphism of C;

        

        thus ((S *' ) . ( id ( dom f))) = ( id (( Obj (S *' )) . ( dom f))) by Lm25

        .= ( id ( cod ((S *' ) . f))) by Lm26;

        

        thus ((S *' ) . ( id ( cod f))) = ( id (( Obj (S *' )) . ( cod f))) by Lm25

        .= ( id ( dom ((S *' ) . f))) by Lm26;

      end;

      let f,g be Morphism of C;

      assume

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

      then

       A2: ( dom (S . g)) = ( cod (S . f)) by CAT_1: 64;

      reconsider Sff = (S . f) as Morphism of ( dom (S . f)), ( cod (S . f)) by CAT_1: 4;

      reconsider Sgg = (S . g) as Morphism of ( dom (S . g)), ( cod (S . g)) by CAT_1: 4;

      

       A3: ( Hom (( dom (S . f)),( cod (S . f)))) <> {} & ( Hom (( dom (S . g)),( cod (S . g)))) <> {} by CAT_1: 2;

      then

       A4: (Sff opp ) = ((S . f) opp ) by Def6;

      

       A5: (Sgg opp ) = ((S . g) opp ) by Def6, A3;

      

      thus ((S *' ) . (g (*) f)) = ((S . (g (*) f)) opp ) by Def11

      .= ((Sgg (*) Sff) opp ) by A1, CAT_1: 64

      .= ((Sff opp ) (*) (Sgg opp )) by A2, Th14, A3

      .= (((S *' ) . f) (*) ((S . g) opp )) by Def11, A4, A5

      .= (((S *' ) . f) (*) ((S *' ) . g)) by Def11;

    end;

    theorem :: OPPCAT_1:59

    for S1 be Contravariant_Functor of C, B, S2 be Functor of B, D holds (S2 * S1) is Contravariant_Functor of C, D

    proof

      let S1 be Contravariant_Functor of C, B, S2 be Functor of B, D;

      ( *' S1) is Functor of (C opp ), B by Th53;

      then (S2 * ( *' S1)) is Functor of (C opp ), D by CAT_1: 73;

      then ( /* (S2 * ( *' S1))) is Contravariant_Functor of C, D by Th32;

      then (S2 * ( /* ( *' S1))) is Contravariant_Functor of C, D by Lm18;

      hence thesis by Th45;

    end;

    theorem :: OPPCAT_1:60

    for S1 be Functor of C, B, S2 be Contravariant_Functor of B, D holds (S2 * S1) is Contravariant_Functor of C, D

    proof

      let S1 be Functor of C, B, S2 be Contravariant_Functor of B, D;

      ( *' S1) is Contravariant_Functor of (C opp ), B by Th55;

      then (S2 * ( *' S1)) is Functor of (C opp ), D by Th33;

      then ( /* (S2 * ( *' S1))) is Contravariant_Functor of C, D by Th32;

      then (S2 * ( /* ( *' S1))) is Contravariant_Functor of C, D by Lm18;

      hence thesis by Th45;

    end;

    theorem :: OPPCAT_1:61

    for F be Functor of C, D, c be Object of C holds (( Obj (( *' F) *' )) . (c opp )) = ((( Obj F) . c) opp )

    proof

      let F be Functor of C, D, c be Object of C;

      ( *' F) is Contravariant_Functor of (C opp ), D by Th55;

      

      hence (( Obj (( *' F) *' )) . (c opp )) = ((( Obj ( *' F)) . (c opp )) opp ) by Th43

      .= ((( Obj F) . ( opp (c opp ))) opp ) by Th38

      .= ((( Obj F) . c) opp );

    end;

    theorem :: OPPCAT_1:62

    for F be Contravariant_Functor of C, D, c be Object of C holds (( Obj (( *' F) *' )) . (c opp )) = ((( Obj F) . c) opp )

    proof

      let F be Contravariant_Functor of C, D, c be Object of C;

      ( *' F) is Functor of (C opp ), D by Th53;

      

      hence (( Obj (( *' F) *' )) . (c opp )) = ((( Obj ( *' F)) . (c opp )) opp ) by Th40

      .= ((( Obj F) . ( opp (c opp ))) opp ) by Th41

      .= ((( Obj F) . c) opp );

    end;

    theorem :: OPPCAT_1:63

    for F be Functor of C, D holds (( *' F) *' ) is Functor of (C opp ), (D opp )

    proof

      let F be Functor of C, D;

      ( *' F) is Contravariant_Functor of (C opp ), D by Th55;

      hence thesis by Th54;

    end;

    theorem :: OPPCAT_1:64

    for F be Contravariant_Functor of C, D holds (( *' F) *' ) is Contravariant_Functor of (C opp ), (D opp )

    proof

      let F be Contravariant_Functor of C, D;

      ( *' F) is Functor of (C opp ), D by Th53;

      hence thesis by Th56;

    end;

    definition

      let C;

      :: OPPCAT_1:def12

      func id* C -> Contravariant_Functor of C, (C opp ) equals (( id C) *' );

      coherence by Th56;

      :: OPPCAT_1:def13

      func *id C -> Contravariant_Functor of (C opp ), C equals ( *' ( id C));

      coherence by Th55;

    end

    theorem :: OPPCAT_1:65

    

     Th63: for f be Morphism of C holds (( id* C) . f) = (f opp )

    proof

      let f be Morphism of C;

      

      thus (( id* C) . f) = ((( id C) . f) opp ) by Def11

      .= (f opp ) by FUNCT_1: 18;

    end;

    theorem :: OPPCAT_1:66

    for c be Object of C holds (( Obj ( id* C)) . c) = (c opp )

    proof

      let c be Object of C;

      

      thus (( Obj ( id* C)) . c) = ((( Obj ( id C)) . c) opp ) by Th40

      .= (c opp ) by CAT_1: 77;

    end;

    theorem :: OPPCAT_1:67

    

     Th65: for f be Morphism of (C opp ) holds (( *id C) . f) = ( opp f)

    proof

      let f be Morphism of (C opp );

      

      thus (( *id C) . f) = (( id C) . ( opp f)) by Def10

      .= ( opp f) by FUNCT_1: 18;

    end;

    theorem :: OPPCAT_1:68

    for c be Object of (C opp ) holds (( Obj ( *id C)) . c) = ( opp c)

    proof

      let c be Object of (C opp );

      

      thus (( Obj ( *id C)) . c) = (( Obj ( id C)) . ( opp c)) by Th38

      .= ( opp c) by CAT_1: 77;

    end;

    theorem :: OPPCAT_1:69

    for S be Function of the carrier' of C, the carrier' of D holds ( *' S) = (S * ( *id C)) & (S *' ) = (( id* D) * S)

    proof

      let S be Function of the carrier' of C, the carrier' of D;

      now

        let f be Morphism of (C opp );

        

        thus (( *' S) . f) = (S . ( opp f)) by Def10

        .= (S . (( *id C) . f)) by Th65

        .= ((S * ( *id C)) . f) by FUNCT_2: 15;

      end;

      hence ( *' S) = (S * ( *id C)) by FUNCT_2: 63;

      now

        let f be Morphism of C;

        

        thus ((S *' ) . f) = ((S . f) opp ) by Def11

        .= (( id* D) . (S . f)) by Th63

        .= ((( id* D) * S) . f) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: OPPCAT_1:70

    for a,b,c be Object of C st ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds (g * f) = ((f opp ) * (g opp )) by Lm3;

    theorem :: OPPCAT_1:71

    

     Th69: for a be Object of C holds ( id a) = ( id (a opp )) by Lm2;

    theorem :: OPPCAT_1:72

    for a be Object of (C opp ) holds ( id a) = ( id ( opp a))

    proof

      let a be Object of (C opp );

      

      thus ( id a) = ( id (( opp a) opp ))

      .= ( id ( opp a)) by Th69;

    end;