:: OPPCAT_1 semantic presentation

begin


definition
let X, Y, Z be non empty set ;
let f be PartFunc of [:X,Y:],Z;
:: original: ~
redefine func ~ f ->  PartFunc of [:Y,X:],Z;
coherence
 ~ f is PartFunc of [:Y,X:],Z by FUNCT_4:48;
end;

definition
let C be Category;
funcC opp  ->  non empty non void strict CatStr  equals :: OPPCAT_1:def 1
 CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);
coherence
 CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is non empty non void strict CatStr ;
end;

:: deftheorem  defines opp OPPCAT_1:def_1_:_
 for C being Category holds C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);

definition
let C be Category;
let c be Object of C;
funcc opp  ->  Object of (C opp) equals :: OPPCAT_1:def 2
c;
coherence
 c is Object of (C opp) ;
end;

:: deftheorem  defines opp OPPCAT_1:def_2_:_
 for C being Category
for c being Object of C holds c opp = c;

registration
let C be Category;
clusterC opp  ->  non empty non void strict Category-like transitive associative reflexive with_identities ;
coherence
 ( C opp is Category-like & C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )
proof
set M = the carrier' of C;
set d = the Target of C;
set c = the Source of C;
set p = ~ the Comp of C;
set B = C opp ;
thus A1: C opp is Category-like ::_thesis: ( C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )
proof
let f, g be Morphism of (C opp); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in dom the Comp of (C opp) or dom g = cod f ) & ( not dom g = cod f or [g,f] in dom the Comp of (C opp) ) )
reconsider ff = f, gg = g as Morphism of C ;
thus  ( [g,f] in dom the Comp of (C opp) implies dom g = cod f ) ::_thesis: ( not dom g = cod f or [g,f] in dom the Comp of (C opp) )
proof
assume  [g,f] in dom the Comp of (C opp) ; ::_thesis: dom g = cod f
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 ; ::_thesis: verum
end;
assume A2: dom g = cod f ; ::_thesis: [g,f] in dom the Comp of (C opp)
 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 (C opp) by FUNCT_4:42; ::_thesis: verum
end;
A3: for f, g being Element of the carrier' of C st the Target of C . g = the Source of C . f holds
(~ the Comp of C) . (g,f) = the Comp of C . (f,g)
proof
let f, g be Element of the carrier' of C; ::_thesis: ( the Target of C . g = the Source of C . f implies (~ the Comp of C) . (g,f) = the Comp of C . (f,g) )
reconsider ff = f, gg = g as Morphism of (C opp) ;
assume  the Target of C . g = the Source of C . f ; ::_thesis: (~ the Comp of C) . (g,f) = the Comp of C . (f,g)
then  dom gg = cod ff ;
then  [gg,ff] in dom (~ the Comp of C) by A1, CAT_1:def_6;
hence  (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by FUNCT_4:43; ::_thesis: verum
end;
thus A4: C opp is transitive ::_thesis: ( C opp is associative & C opp is reflexive & C opp is with_identities )
proof
let ff, gg be Morphism of (C opp); :: according to CAT_1:def_7 ::_thesis: ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
reconsider f = ff, g = gg as Morphism of C ;
assume A5: dom gg = cod ff ; ::_thesis: ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
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 (C opp) by A5, A1, CAT_1:def_6;
then A8: gg (*) ff = (~ the Comp of C) . (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 ;
::_thesis: cod (gg (*) ff) = cod gg
thus  cod (gg (*) ff) = dom (f (*) g) by A8
.= dom g by A6, CAT_1:def_7
.= cod gg ; ::_thesis: verum
end;
thus  C opp is associative ::_thesis: ( C opp is reflexive & C opp is with_identities )
proof
let ff, gg, hh be Morphism of (C opp); :: according to CAT_1:def_8 ::_thesis: ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
reconsider f = ff, g = gg, h = hh as Morphism of C ;
assume that
A9: dom hh = cod gg and
A10: dom gg = cod ff ; ::_thesis: hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
A11: [h,g] in dom (~ the Comp of C) by A1, CAT_1:def_6, A9;
then A12: (~ the Comp of C) . (h,g) is Element of the carrier' of C by PARTFUN1:4;
A13: [g,f] in dom (~ the Comp of C) by A1, CAT_1:def_6, A10;
then A14: (~ the Comp of C) . (g,f) is Element of the carrier' of C by PARTFUN1:4;
A15: (~ the Comp of C) . (h,g) = the Comp of C . (g,h) by A3, A9;
the Target of C . ((~ the Comp of C) . (h,g)) = dom (hh (*) gg) by A11, CAT_1:def_1
.= dom gg by A4, CAT_1:def_7, A9 ;
then A16: (~ the Comp of C) . (((~ the Comp of C) . (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: (~ the Comp of C) . (g,f) = the Comp of C . (f,g) by A3, A10;
A19: the Source of C . ((~ the Comp of C) . (g,f)) = cod (gg (*) ff) by A13, CAT_1:def_1
.= cod gg by A4, CAT_1:def_7, A10 ;
 dom (hh (*) gg) = dom gg by A4, CAT_1:def_7, A9;
then A20: [(hh (*) gg),ff] in dom the Comp of (C opp) by A1, CAT_1:def_6, A10;
 cod (gg (*) ff) = cod gg by A4, CAT_1:def_7, A10;
then A21: [hh,(gg (*) ff)] in dom the Comp of (C opp) by A1, CAT_1:def_6, A9;
 [hh,gg] in dom the Comp of (C opp) by A9, A1, CAT_1:def_6;
then A22: hh (*) gg = (~ the Comp of C) . (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 (C opp) by A10, A1, CAT_1:def_6;
then  gg (*) ff = (~ the Comp of C) . (g,f) by CAT_1:def_1;
hence hh (*) (gg (*) ff) = (~ the Comp of C) . (h,((~ the Comp of C) . (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
.= (~ the Comp of C) . (((~ the Comp of C) . (h,g)),f) by A16, A17, A25, A26, CAT_1:16
.= (hh (*) gg) (*) ff by A20, A22, CAT_1:def_1 ;
::_thesis: verum
end;
thus  C opp is reflexive ::_thesis: C opp is with_identities
proof
let bb be Object of (C opp); :: according to CAT_1:def_9 ::_thesis: not Hom (bb,bb) = {}
reconsider b = bb as Element of C ;
consider f being Morphism of C such that
A27: f in Hom (b,b) by SUBSET_1:4;
reconsider ff = f as Morphism of (C opp) ;
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) <> {} ; ::_thesis: verum
end;
let a be Element of (C opp); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (C opp) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of C ;
reconsider ii = id aa as Morphism of (C opp) ;
A29: dom ii = cod (id aa)
.= aa ;
A30: cod ii = dom (id aa)
.= aa ;
then reconsider ii = ii as Morphism of a,a by A29, CAT_1:4;
take  ii ; ::_thesis: for b1 being Element of the carrier of (C opp) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be Element of (C opp); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
reconsider bb = b as Element of C ;
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A31: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; ::_thesis: g (*) ii = g
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 = gg as Morphism of bb,aa by A32, A33, CAT_1:4;
A35: the Source of C . ii = aa by A30
.= dom g by A31, CAT_1:5
.= the Target of C . g ;
then  dom g = cod ii ;
then  [g,ii] in dom the Comp of (C opp) by A1, CAT_1:def_6;
hence g (*) ii = (~ the Comp of C) . (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 ;
::_thesis: verum
end;
assume A36: Hom (b,a) <> {} ; ::_thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1
let g be Morphism of b,a; ::_thesis: ii (*) g = g
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 = gg as Morphism of aa,bb by A37, A38, CAT_1:4;
A40: the Target of C . ii = aa by A29
.= cod g by A36, CAT_1:5
.= the Source of C . g ;
then  cod g = dom ii ;
then  [ii,g] in dom the Comp of (C opp) by A1, CAT_1:def_6;
hence ii (*) g = (~ the Comp of C) . (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 ;
::_thesis: verum
end;
end;

definition
let C be Category;
let c be Object of (C opp);
func opp c ->  Object of C equals :: OPPCAT_1:def 3
c opp ;
coherence
 c opp is Object of C ;
end;

:: deftheorem  defines opp OPPCAT_1:def_3_:_
 for C being Category
for c being Object of (C opp) holds opp c = c opp ;

theorem :: OPPCAT_1:1
canceled;

theorem :: OPPCAT_1:2
for C being Category
for c being Object of C holds (c opp) opp = c ;

theorem :: OPPCAT_1:3
for C being Category
for c being Object of C holds opp (c opp) = c ;

theorem :: OPPCAT_1:4
for C being Category
for c being Object of (C opp) holds (opp c) opp = c ;

theorem Th5: :: OPPCAT_1:5
for C being Category
for a, b being Object of C holds Hom (a,b) = Hom ((b opp),(a opp))
proof
let C be Category; ::_thesis: for a, b being Object of C holds Hom (a,b) = Hom ((b opp),(a opp))
let a, b be Object of C; ::_thesis: Hom (a,b) = Hom ((b opp),(a opp))
thus  Hom (a,b) c= Hom ((b opp),(a opp)) :: according to XBOOLE_0:def_10 ::_thesis: Hom ((b opp),(a opp)) c= Hom (a,b)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom ((b opp),(a opp)) )
assume A1: x in Hom (a,b) ; ::_thesis: x in Hom ((b opp),(a opp))
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)) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom ((b opp),(a opp)) or x in Hom (a,b) )
assume A2: x in Hom ((b opp),(a opp)) ; ::_thesis: x in Hom (a,b)
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) ; ::_thesis: verum
end;

theorem Th6: :: OPPCAT_1:6
for C being Category
for a, b being Object of (C opp) holds Hom (a,b) = Hom ((opp b),(opp a))
proof
let C be Category; ::_thesis: for a, b being Object of (C opp) holds Hom (a,b) = Hom ((opp b),(opp a))
let a, b be Object of (C opp); ::_thesis: Hom (a,b) = Hom ((opp b),(opp a))
thus  Hom (a,b) = Hom (((opp a) opp),((opp b) opp))
.= Hom ((opp b),(opp a)) by Th5 ; ::_thesis: verum
end;

definition
let C be Category;
let f be Morphism of C;
funcf opp  ->  Morphism of (C opp) equals :: OPPCAT_1:def 4
f;
coherence
 f is Morphism of (C opp) ;
end;

:: deftheorem  defines opp OPPCAT_1:def_4_:_
 for C being Category
for f being Morphism of C holds f opp = f;

definition
let C be Category;
let f be Morphism of (C opp);
func opp f ->  Morphism of C equals :: OPPCAT_1:def 5
f opp ;
coherence
 f opp is Morphism of C ;
end;

:: deftheorem  defines opp OPPCAT_1:def_5_:_
 for C being Category
for f being Morphism of (C opp) holds opp f = f opp ;

definition
let C be Category;
let a, b be Object of C;
assume Z: Hom (a,b) <> {} ;
let f be Morphism of a,b;
funcf opp  ->  Morphism of b opp ,a opp  equals :Def6: :: OPPCAT_1:def 6
f;
coherence
 f is Morphism of b opp ,a opp
proof
 f in Hom (a,b) by Z, CAT_1:def_5;
then  f in Hom ((b opp),(a opp)) by Th5;
hence  f is Morphism of b opp ,a opp by CAT_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines opp OPPCAT_1:def_6_:_
 for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds f opp = f;

definition
let C be Category;
let a, b be Object of C;
assume Z: Hom ((a opp),(b opp)) <> {} ;
let f be Morphism of a opp ,b opp ;
func opp f ->  Morphism of b,a equals :Def7: :: OPPCAT_1:def 7
f;
coherence
 f is Morphism of b,a
proof
 f in Hom ((a opp),(b opp)) by Z, CAT_1:def_5;
then  f in Hom (b,a) by Th5;
hence  f is Morphism of b,a by CAT_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines opp OPPCAT_1:def_7_:_
 for C being Category
for a, b being Object of C st Hom ((a opp),(b opp)) <> {} holds
for f being Morphism of a opp ,b opp holds opp f = f;

theorem :: OPPCAT_1:7
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (f opp) opp = f
proof
let C be Category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (f opp) opp = f
let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (f opp) opp = f )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds (f opp) opp = f
then A2: Hom ((b opp),(a opp)) <> {} by Th5;
let f be Morphism of a,b; ::_thesis: (f opp) opp = f
thus (f opp) opp = f opp by A2, Def6
.= f by A1, Def6 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:8
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds opp (f opp) = f
proof
let C be Category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds opp (f opp) = f
let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds opp (f opp) = f )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds opp (f opp) = f
then A2: Hom ((b opp),(a opp)) <> {} by Th5;
let f be Morphism of a,b; ::_thesis: opp (f opp) = f
thus  opp (f opp) = f opp by A2, Def7
.= f by A1, Def6 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:9
for C being Category
for a, b being Object of (C opp)
for f being Morphism of a,b holds (opp f) opp = f ;

theorem Th10: :: OPPCAT_1:10
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( dom (f opp) = cod f & cod (f opp) = dom f )
proof
let C be Category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( dom (f opp) = cod f & cod (f opp) = dom f )
let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds
( dom (f opp) = cod f & cod (f opp) = dom f ) )
assume A1: Hom (a,b) <> {} ; ::_thesis: for f being Morphism of a,b holds
( dom (f opp) = cod f & cod (f opp) = dom f )
then A2: Hom ((b opp),(a opp)) <> {} by Th5;
let f be Morphism of a,b; ::_thesis: ( dom (f opp) = cod f & cod (f opp) = dom f )
thus  dom (f opp) = b by A2, CAT_1:5
.= cod f by A1, CAT_1:5 ; ::_thesis: cod (f opp) = dom f
thus  cod (f opp) = a by A2, CAT_1:5
.= dom f by A1, CAT_1:5 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:11
for C being Category
for a, b being Object of (C opp)
for f being Morphism of a,b holds
( dom (opp f) = cod f & cod (opp f) = dom f ) ;

theorem :: OPPCAT_1:12
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( (dom f) opp = cod (f opp) & (cod f) opp = dom (f opp) ) by Th10;

theorem :: OPPCAT_1:13
for C being Category
for a, b being Object of (C opp) st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( opp (dom f) = cod (opp f) & opp (cod f) = dom (opp f) ) ;

theorem :: OPPCAT_1:14
canceled;

theorem Th15: :: OPPCAT_1:15
for C being Category
for a, b being Object of (C opp)
for f being Morphism of a,b st Hom (a,b) <> {} holds
opp f is Morphism of opp b, opp a
proof
let C be Category; ::_thesis: for a, b being Object of (C opp)
for f being Morphism of a,b st Hom (a,b) <> {} holds
opp f is Morphism of opp b, opp a
let a, b be Object of (C opp); ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds
opp f is Morphism of opp b, opp a
let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies opp f is Morphism of opp b, opp a )
assume  Hom (a,b) <> {} ; ::_thesis: opp f is Morphism of opp b, opp a
then  f in Hom (a,b) by CAT_1:def_5;
then  opp f in Hom ((opp b),(opp a)) by Th6;
hence  opp f is Morphism of opp b, opp a by CAT_1:def_5; ::_thesis: verum
end;

theorem Th16: :: OPPCAT_1:16
for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
proof
let C be Category; ::_thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
let a, b, c be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
A3: Hom ((b opp),(a opp)) <> {} by A1, Th5;
A4: Hom ((c opp),(b opp)) <> {} by A2, Th5;
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
let g be Morphism of b,c; ::_thesis: (g (*) f) opp = (f opp) (*) (g opp)
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, CAT_1:15, FUNCT_4:53, A8;
then  the Comp of C . (g,f) = the Comp of (C opp) . ((f opp),(g opp)) by FUNCT_4:def_2, A7;
hence  (g (*) f) opp = (f opp) (*) (g opp) by A5, A6, A8, CAT_1:16, A9; ::_thesis: verum
end;

theorem :: OPPCAT_1:17
for C being Category
for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
proof
let C be Category; ::_thesis: for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
let a, b, c be Object of C; ::_thesis: ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) )
assume  ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
then  ( Hom (a,b) <> {} & Hom (b,c) <> {} ) by Th5;
hence  for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp) by Th16; ::_thesis: verum
end;

theorem Th18: :: OPPCAT_1:18
for C being Category
for f, g being Morphism of (C opp) st dom g = cod f holds
opp (g (*) f) = (opp f) (*) (opp g)
proof
let C be Category; ::_thesis: for f, g being Morphism of (C opp) st dom g = cod f holds
opp (g (*) f) = (opp f) (*) (opp g)
let f, g be Morphism of (C opp); ::_thesis: ( dom g = cod f implies opp (g (*) f) = (opp f) (*) (opp g) )
assume A1: dom g = cod f ; ::_thesis: opp (g (*) f) = (opp f) (*) (opp g)
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 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:19
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
proof
let C be Category; ::_thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
let a, b, c be Object of C; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
let g be Morphism of b,c; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies (g * f) opp = (f opp) (*) (g opp) )
assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; ::_thesis: (g * f) opp = (f opp) (*) (g opp)
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, Th16 ; ::_thesis: verum
end;

Lm1:  for C being Category
for a being Object of C
for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
proof
let C be Category; ::_thesis: for a being Object of C
for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
let a be Object of C; ::_thesis: for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
let b be Object of (C opp); ::_thesis: ( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
thus  ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) ::_thesis: ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f )
proof
assume A1: Hom ((a opp),b) <> {} ; ::_thesis: for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f
A2: Hom ((opp b),(opp (a opp))) <> {} by A1, Th6;
let f be Morphism of a opp ,b; ::_thesis: f (*) ((id a) opp) = f
A3: Hom (a,a) <> {} ;
A4: cod (opp f) = dom f
.= a by CAT_1:5, A1 ;
dom (opp f) = cod f
.= opp b by CAT_1:5, A1 ;
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, Th16
.= ((id a) * ff) opp by A5, Def6, A2
.= ff opp by CAT_1:28, A2
.= f by A2, Def6 ; ::_thesis: verum
end;
assume A6: Hom (b,(a opp)) <> {} ; ::_thesis: for f being Morphism of b,a opp holds ((id a) opp) (*) f = f
A7: Hom ((opp (a opp)),(opp b)) <> {} by A6, Th6;
let f be Morphism of b,a opp ; ::_thesis: ((id a) opp) (*) f = f
A8: Hom (a,a) <> {} ;
A9: dom (opp f) = cod f
.= a by CAT_1:5, A6 ;
cod (opp f) = dom f
.= opp b by CAT_1:5, A6 ;
then reconsider ff = opp f 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, Th16
.= (ff * (id a)) opp by A10, Def6, A7
.= ff opp by CAT_1:29, A7
.= f by A7, Def6 ; ::_thesis: verum
end;

theorem Th20: :: OPPCAT_1:20
for C being Category
for a being Object of C holds (id a) opp = id (a opp)
proof
let C be Category; ::_thesis: for a being Object of C holds (id a) opp = id (a opp)
let a be Object of C; ::_thesis: (id a) opp = id (a opp)
 for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being 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; ::_thesis: verum
end;

Lm2:  for C being Category
for a being Object of C holds id a = id (a opp)
proof
let C be Category; ::_thesis: for a being Object of C holds id a = id (a opp)
let a be Object of C; ::_thesis: id a = id (a opp)
 Hom (a,a) <> {} ;
hence  id a = (id a) opp by Def6
.= id (a opp) by Th20 ;
::_thesis: verum
end;

theorem Th21: :: OPPCAT_1:21
for C being Category
for a being Object of (C opp) holds opp (id a) = id (opp a)
proof
let C be Category; ::_thesis: for a being Object of (C opp) holds opp (id a) = id (opp a)
let a be Object of (C opp); ::_thesis: opp (id a) = id (opp a)
set b = opp a;
thus  opp (id a) = id ((opp a) opp)
.= id (opp a) by Lm2 ; ::_thesis: verum
end;

Lm3:  for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (f opp) * (g opp)
proof
let C be Category; ::_thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (f opp) * (g opp)
let a, b, c be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (f opp) * (g opp) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (f opp) * (g opp)
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds g * f = (f opp) * (g opp)
let g be Morphism of b,c; ::_thesis: g * f = (f opp) * (g opp)
reconsider f1 = f as Morphism of C ;
reconsider g1 = g as Morphism of C ;
A3: Hom ((b opp),(a opp)) <> {} by A1, Th5;
A4: Hom ((c opp),(b opp)) <> {} by A2, Th5;
g * f = (g (*) f) opp by A1, A2, CAT_1:def_13
.= (f opp) (*) (g opp) by A1, A2, Th16
.= (f opp) * (g opp) by A3, A4, CAT_1:def_13 ;
hence  g * f = (f opp) * (g opp) ; ::_thesis: verum
end;

theorem :: OPPCAT_1:22
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f opp is monic iff f is epi )
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b holds
( f opp is monic iff f is epi )
let a, b be Object of C; ::_thesis: for f being Morphism of a,b holds
( f opp is monic iff f is epi )
let f be Morphism of a,b; ::_thesis: ( f opp is monic iff f is epi )
thus  ( f opp is monic implies f is epi ) ::_thesis: ( f is epi implies f opp is monic )
proof
assume that
A1: Hom ((b opp),(a opp)) <> {} and
A2: for c being Object of (C opp) st Hom (c,(b opp)) <> {} holds
for f1, f2 being Morphism of c,b opp st (f opp) * f1 = (f opp) * f2 holds
f1 = f2 ; :: according to CAT_1:def_14 ::_thesis: f is epi
thus A3: Hom (a,b) <> {} by A1, Th5; :: according to CAT_1:def_15 ::_thesis: for b1 being Element of the carrier of C holds
( Hom (b,b1) = {} or for b2, b3 being Morphism of b,b1 holds
( not b2 * f = b3 * f or b2 = b3 ) )
let c be Object of C; ::_thesis: ( Hom (b,c) = {} or for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 ) )
assume A4: Hom (b,c) <> {} ; ::_thesis: for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 )
let g1, g2 be Morphism of b,c; ::_thesis: ( not g1 * f = g2 * f or g1 = g2 )
assume A5: g1 * f = g2 * f ; ::_thesis: g1 = g2
reconsider f1 = g1 opp , f2 = g2 opp as Morphism of c opp ,b opp ;
A6: Hom ((c opp),(b opp)) <> {} by A4, Th5;
(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  g1 = g2 ; ::_thesis: verum
end;
assume that
A8: Hom (a,b) <> {} and
A9: for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ; :: according to CAT_1:def_15 ::_thesis: f opp is monic
thus  Hom ((b opp),(a opp)) <> {} by A8, Th5; :: according to CAT_1:def_14 ::_thesis: for b1 being Element of the carrier of (C opp) holds
( Hom (b1,(b opp)) = {} or for b2, b3 being Morphism of b1,b opp holds
( not (f opp) * b2 = (f opp) * b3 or b2 = b3 ) )
let c be Object of (C opp); ::_thesis: ( Hom (c,(b opp)) = {} or for b1, b2 being Morphism of c,b opp holds
( not (f opp) * b1 = (f opp) * b2 or b1 = b2 ) )
assume A10: Hom (c,(b opp)) <> {} ; ::_thesis: for b1, b2 being Morphism of c,b opp holds
( not (f opp) * b1 = (f opp) * b2 or b1 = b2 )
let f1, f2 be Morphism of c,b opp ; ::_thesis: ( not (f opp) * f1 = (f opp) * f2 or f1 = f2 )
assume A11: (f opp) * f1 = (f opp) * f2 ; ::_thesis: f1 = 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 Th6;
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, Th6;
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; ::_thesis: verum
end;

theorem :: OPPCAT_1:23
for C being Category
for b, c being Object of C st Hom (b,c) <> {} holds
for f being Morphism of b,c holds
( f opp is epi iff f is monic )
proof
let C be Category; ::_thesis: for b, c being Object of C st Hom (b,c) <> {} holds
for f being Morphism of b,c holds
( f opp is epi iff f is monic )
let b, c be Object of C; ::_thesis: ( Hom (b,c) <> {} implies for f being Morphism of b,c holds
( f opp is epi iff f is monic ) )
assume A1: Hom (b,c) <> {} ; ::_thesis: for f being Morphism of b,c holds
( f opp is epi iff f is monic )
let f be Morphism of b,c; ::_thesis: ( f opp is epi iff f is monic )
thus  ( f opp is epi implies f is monic ) ::_thesis: ( f is monic implies f opp is epi )
proof
assume that
 Hom ((c opp),(b opp)) <> {} and
A2: for a being Object of (C opp) st Hom ((b opp),a) <> {} holds
for g1, g2 being Morphism of b opp ,a st g1 * (f opp) = g2 * (f opp) holds
g1 = g2 ; :: according to CAT_1:def_15 ::_thesis: f is monic
thus  Hom (b,c) <> {} by A1; :: according to CAT_1:def_14 ::_thesis: for b1 being Element of the carrier of C holds
( Hom (b1,b) = {} or for b2, b3 being Morphism of b1,b holds
( not f * b2 = f * b3 or b2 = b3 ) )
let a be Object of C; ::_thesis: ( Hom (a,b) = {} or for b1, b2 being Morphism of a,b holds
( not f * b1 = f * b2 or b1 = b2 ) )
assume A3: Hom (a,b) <> {} ; ::_thesis: for b1, b2 being Morphism of a,b holds
( not f * b1 = f * b2 or b1 = b2 )
let f1, f2 be Morphism of a,b; ::_thesis: ( not f * f1 = f * f2 or f1 = f2 )
assume A4: f * f1 = f * f2 ; ::_thesis: f1 = f2
reconsider g1 = f1 opp , g2 = f2 opp as Morphism of b opp ,a opp ;
A5: Hom ((b opp),(a opp)) <> {} by A3, Th5;
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 ;
::_thesis: verum
end;
assume that
A6: Hom (b,c) <> {} and
A7: for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st f * f1 = f * f2 holds
f1 = f2 ; :: according to CAT_1:def_14 ::_thesis: f opp is epi
thus  Hom ((c opp),(b opp)) <> {} by A6, Th5; :: according to CAT_1:def_15 ::_thesis: for b1 being Element of the carrier of (C opp) holds
( Hom ((b opp),b1) = {} or for b2, b3 being Morphism of b opp ,b1 holds
( not b2 * (f opp) = b3 * (f opp) or b2 = b3 ) )
let a be Object of (C opp); ::_thesis: ( Hom ((b opp),a) = {} or for b1, b2 being Morphism of b opp ,a holds
( not b1 * (f opp) = b2 * (f opp) or b1 = b2 ) )
assume A8: Hom ((b opp),a) <> {} ; ::_thesis: for b1, b2 being Morphism of b opp ,a holds
( not b1 * (f opp) = b2 * (f opp) or b1 = b2 )
let g1, g2 be Morphism of b opp ,a; ::_thesis: ( not g1 * (f opp) = g2 * (f opp) or g1 = g2 )
assume A9: g1 * (f opp) = g2 * (f opp) ; ::_thesis: g1 = g2
Hom ((b opp),a) = Hom ((opp a),(opp (b opp))) by Th6
.= 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, Th6;
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  g1 = g2 by A7, A10; ::_thesis: verum
end;

theorem :: OPPCAT_1:24
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )
proof
let C be Category; ::_thesis: for a, b being Object of C
for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )
let a, b be Object of C; ::_thesis: for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )
let f be Morphism of a,b; ::_thesis: ( f opp is invertible iff f is invertible )
thus  ( f opp is invertible implies f is invertible ) ::_thesis: ( f is invertible implies f opp is invertible )
proof
assume A1: ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) ; :: according to CAT_1:def_16 ::_thesis: ( for b1 being Morphism of a opp ,b opp holds
( not (f opp) * b1 = id (a opp) or not b1 * (f opp) = id (b opp) ) or f is invertible )
given gg being Morphism of a opp ,b opp  such that A2: ( (f opp) * gg = id (a opp) & gg * (f opp) = id (b opp) ) ; ::_thesis: f is invertible
thus A3: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, Th5; :: according to CAT_1:def_16 ::_thesis: ex b1 being Morphism of b,a st
( f * b1 = id b & b1 * f = id a )
reconsider g = opp gg as Morphism of b,a ;
take  g ; ::_thesis: ( f * g = id b & g * f = id a )
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 ; ::_thesis: g * f = id a
thus g * f = (f opp) * (g opp) by A3, Lm3
.= id a by A2, A4, Lm2 ; ::_thesis: verum
end;
assume A5: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_1:def_16 ::_thesis: ( for b1 being Morphism of b,a holds
( not f * b1 = id b or not b1 * f = id a ) or f opp is invertible )
given g being Morphism of b,a such that A6: ( f * g = id b & g * f = id a ) ; ::_thesis: f opp is invertible
thus  ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A5, Th5; :: according to CAT_1:def_16 ::_thesis: ex b1 being Morphism of a opp ,b opp st
( (f opp) * b1 = id (a opp) & b1 * (f opp) = id (b opp) )
take  g opp ; ::_thesis: ( (f opp) * (g opp) = id (a opp) & (g opp) * (f opp) = id (b opp) )
thus (f opp) * (g opp) = g * f by A5, Lm3
.= id (a opp) by A6, Lm2 ; ::_thesis: (g opp) * (f opp) = id (b opp)
thus (g opp) * (f opp) = f * g by A5, Lm3
.= id (b opp) by A6, Lm2 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:25
for C being Category
for c being Object of C holds
( c is initial iff c opp is terminal )
proof
let C be Category; ::_thesis: for c being Object of C holds
( c is initial iff c opp is terminal )
let c be Object of C; ::_thesis: ( c is initial iff c opp is terminal )
thus  ( c is initial implies c opp is terminal ) ::_thesis: ( c opp is terminal implies c is initial )
proof
assume A1: c is initial ; ::_thesis: c opp is terminal
let b be Object of (C opp); :: according to CAT_1:def_18 ::_thesis: ( not Hom (b,(c opp)) = {} & ex b1 being Morphism of b,c opp st
for b2 being Morphism of b,c opp holds b1 = b2 )
consider f being Morphism of c, opp b such that
A2: for g being Morphism of c, opp b holds f = g by A1, CAT_1:def_19;
A3: (opp b) opp = b ;
A4: Hom (c,(opp b)) <> {} by A1, CAT_1:def_19;
reconsider f9 = f opp as Morphism of b,c opp ;
thus A5: Hom (b,(c opp)) <> {} by A3, Th5, A4; ::_thesis: ex b1 being Morphism of b,c opp st
for b2 being Morphism of b,c opp holds b1 = b2
take  f9 ; ::_thesis: for b1 being Morphism of b,c opp holds f9 = b1
let g be Morphism of b,c opp ; ::_thesis: f9 = g
 opp (c opp) = c ;
then  opp g is Morphism of c, opp b by A5, Th15;
hence g = f by A2
.= f9 by A4, Def6 ;
::_thesis: verum
end;
assume A6: c opp is terminal ; ::_thesis: c is initial
let b be Object of C; :: according to CAT_1:def_19 ::_thesis: ( not Hom (c,b) = {} & ex b1 being Morphism of c,b st
for b2 being Morphism of c,b holds b1 = b2 )
consider f being Morphism of b opp ,c opp  such that
A7: for g being Morphism of b opp ,c opp holds f = g by A6, CAT_1:def_18;
A8: ( opp (c opp) = c & opp (b opp) = b ) ;
A9: Hom ((b opp),(c opp)) <> {} by A6, CAT_1:def_18;
reconsider f9 = opp f as Morphism of c,b ;
thus A10: Hom (c,b) <> {} by A8, Th6, A9; ::_thesis: ex b1 being Morphism of c,b st
for b2 being Morphism of c,b holds b1 = b2
take  f9 ; ::_thesis: for b1 being Morphism of c,b holds f9 = b1
let g be Morphism of c,b; ::_thesis: f9 = g
 g opp = f by A7;
hence g = f by Def6, A10
.= f9 by A9, Def7 ;
::_thesis: verum
end;

theorem :: OPPCAT_1:26
for C being Category
for c being Object of C holds
( c opp is initial iff c is terminal )
proof
let C be Category; ::_thesis: for c being Object of C holds
( c opp is initial iff c is terminal )
let c be Object of C; ::_thesis: ( c opp is initial iff c is terminal )
thus  ( c opp is initial implies c is terminal ) ::_thesis: ( c is terminal implies c opp is initial )
proof
assume A1: c opp is initial ; ::_thesis: c is terminal
let b be Object of C; :: according to CAT_1:def_18 ::_thesis: ( not Hom (b,c) = {} & ex b1 being Morphism of b,c st
for b2 being Morphism of b,c holds b1 = b2 )
consider f being Morphism of c opp ,b opp  such that
A2: for g being Morphism of c opp ,b opp holds f = g by A1, CAT_1:def_19;
A3: ( opp (b opp) = b & opp (c opp) = c ) ;
A4: Hom ((c opp),(b opp)) <> {} by A1, CAT_1:def_19;
reconsider f9 = opp f as Morphism of b,c ;
thus A5: Hom (b,c) <> {} by A3, Th6, A4; ::_thesis: ex b1 being Morphism of b,c st
for b2 being Morphism of b,c holds b1 = b2
take  f9 ; ::_thesis: for b1 being Morphism of b,c holds f9 = b1
let g be Morphism of b,c; ::_thesis: f9 = g
 g opp = f by A2;
hence g = f by A5, Def6
.= f9 by Def7, A4 ;
::_thesis: verum
end;
assume A6: c is terminal ; ::_thesis: c opp is initial
let b be Object of (C opp); :: according to CAT_1:def_19 ::_thesis: ( not Hom ((c opp),b) = {} & ex b1 being Morphism of c opp ,b st
for b2 being Morphism of c opp ,b holds b1 = b2 )
consider f being Morphism of opp b,c such that
A7: for g being Morphism of opp b,c holds f = g by A6, CAT_1:def_18;
A8: (opp b) opp = b ;
A9: Hom ((opp b),c) <> {} by A6, CAT_1:def_18;
reconsider f9 = f opp as Morphism of c opp ,b ;
thus A10: Hom ((c opp),b) <> {} by A8, Th5, A9; ::_thesis: ex b1 being Morphism of c opp ,b st
for b2 being Morphism of c opp ,b holds b1 = b2
take  f9 ; ::_thesis: for b1 being Morphism of c opp ,b holds f9 = b1
let g be Morphism of c opp ,b; ::_thesis: f9 = g
 opp g is Morphism of opp b, opp (c opp) by A10, Th15;
hence g = f by A7
.= f9 by Def6, A9 ;
::_thesis: verum
end;

definition
let C, B be Category;
let S be Function of the carrier' of (C opp), the carrier' of B;
func /* S ->  Function of the carrier' of C, the carrier' of B means :Def8: :: OPPCAT_1:def 8
 for f being Morphism of C holds it . f = S . (f opp);
existence
 ex b1 being Function of the carrier' of C, the carrier' of B st
for f being Morphism of C holds b1 . f = S . (f opp)
proof
deffunc H1( Morphism of C) ->  Element of the carrier' of B = S . ($1 opp);
thus  ex F being Function of the carrier' of C, the carrier' of B st
for f being Morphism of C holds F . f = H1(f) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier' of C, the carrier' of B st ( for f being Morphism of C holds b1 . f = S . (f opp) ) & ( for f being Morphism of C holds b2 . f = S . (f opp) ) holds
b1 = b2
proof
let T1, T2 be Function of the carrier' of C, the carrier' of B; ::_thesis: ( ( for f being Morphism of C holds T1 . f = S . (f opp) ) & ( for f being Morphism of C holds T2 . f = S . (f opp) ) implies T1 = T2 )
assume that
A1: for f being Morphism of C holds T1 . f = S . (f opp) and
A2: for f being Morphism of C holds T2 . f = S . (f opp) ; ::_thesis: T1 = T2
now__::_thesis:_for_f_being_Morphism_of_C_holds_T1_._f_=_T2_._f
let f be Morphism of C; ::_thesis: T1 . f = T2 . f
thus T1 . f = S . (f opp) by A1
.= T2 . f by A2 ; ::_thesis: verum
end;
hence  T1 = T2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines /* OPPCAT_1:def_8_:_
 for C, B being Category
for S being Function of the carrier' of (C opp), the carrier' of B
for b4 being Function of the carrier' of C, the carrier' of B holds
( b4 = /* S iff for f being Morphism of C holds b4 . f = S . (f opp) );

theorem :: OPPCAT_1:27
for C, B being Category
for S being Function of the carrier' of (C opp), the carrier' of B
for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f
proof
let C, B be Category; ::_thesis: for S being Function of the carrier' of (C opp), the carrier' of B
for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f
let S be Function of the carrier' of (C opp), the carrier' of B; ::_thesis: for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f
let f be Morphism of (C opp); ::_thesis: (/* S) . (opp f) = S . f
thus (/* S) . (opp f) = S . ((opp f) opp) by Def8
.= S . f ; ::_thesis: verum
end;

Lm4:  for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
proof
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
let S be Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj S) . (c opp))
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 Th20
.= id ((Obj S) . (c opp)) by CAT_1:68 ; ::_thesis: verum
end;

theorem Th28: :: OPPCAT_1:28
for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
proof
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
let S be Functor of C opp ,B; ::_thesis: for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
let c be Object of C; ::_thesis: (Obj (/* S)) . c = (Obj S) . (c opp)
A1: now__::_thesis:_for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d
let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d
 (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm4;
hence  ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum
end;
 (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm4;
hence  (Obj (/* S)) . c = (Obj S) . (c opp) by A1, CAT_1:66; ::_thesis: verum
end;

theorem :: OPPCAT_1:29
for C, B being Category
for S being Functor of C opp ,B
for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
proof
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
let S be Functor of C opp ,B; ::_thesis: for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
let c be Object of (C opp); ::_thesis: (Obj (/* S)) . (opp c) = (Obj S) . c
thus (Obj (/* S)) . (opp c) = (Obj S) . ((opp c) opp) by Th28
.= (Obj S) . c ; ::_thesis: verum
end;

Lm5:  for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
proof
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
let S be Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj (/* S)) . 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 Th20
.= id ((Obj S) . (c opp)) by CAT_1:68
.= id ((Obj (/* S)) . c) by Th28 ; ::_thesis: verum
end;

Lm6: now__::_thesis:_for_C,_B_being_Category
for_S_being_Functor_of_C_opp_,B
for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for c being Object of C ex d being Object of B st (/* S) . (id c) = id d
let S be Functor of C opp ,B; ::_thesis: for c being Object of C ex d being Object of B st (/* S) . (id c) = id d
let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d
 (/* S) . (id c) = id ((Obj (/* S)) . c) by Lm5;
hence  ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum
end;

Lm7:  for C, B being Category
for S being Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) )
proof
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) )
let S be Functor of C opp ,B; ::_thesis: for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) )
let f be Morphism of C; ::_thesis: ( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) )
A1: (Obj (/* S)) . (cod f) = (Obj S) . ((cod f) opp) by Th28
.= (Obj S) . (dom (f opp))
.= dom (S . (f opp)) by CAT_1:69 ;
(Obj (/* S)) . (dom f) = (Obj S) . ((dom f) opp) by Th28
.= (Obj S) . (cod (f opp))
.= cod (S . (f opp)) by CAT_1:69 ;
hence  ( (Obj (/* S)) . (dom f) = cod ((/* S) . f) & (Obj (/* S)) . (cod f) = dom ((/* S) . f) ) by A1, Def8; ::_thesis: verum
end;

Lm8: now__::_thesis:_for_C,_B_being_Category
for_S_being_Functor_of_C_opp_,B
for_f_being_Morphism_of_C_holds_
(_(/*_S)_._(id_(dom_f))_=_id_(cod_((/*_S)_._f))_&_(/*_S)_._(id_(cod_f))_=_id_(dom_((/*_S)_._f))_)
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )
let S be Functor of C opp ,B; ::_thesis: for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )
let f be Morphism of C; ::_thesis: ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )
thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm5
.= id (cod ((/* S) . f)) by Lm7 ; ::_thesis: (/* S) . (id (cod f)) = id (dom ((/* S) . f))
thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm5
.= id (dom ((/* S) . f)) by Lm7 ; ::_thesis: verum
end;

Lm9:  for C, B being Category
for S being Functor of C opp ,B
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
proof
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
let S be Functor of C opp ,B; ::_thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
let a, b, c be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) )
assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; ::_thesis: for f being Morphism of a,b
for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
A2: ( Hom ((b opp),(a opp)) <> {} & Hom ((c opp),(b opp)) <> {} ) by A1, Th5;
let f be Morphism of a,b; ::_thesis: for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
let g be Morphism of b,c; ::_thesis: (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
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 opp) by A1, Def6
.= (/* S) . f by Def8 ;
A7: S . (g opp) = S . (g opp) by A1, Def6
.= (/* S) . g by Def8 ;
thus (/* S) . (g (*) f) = S . ((g (*) f) opp) by Def8
.= S . ((f opp) (*) (g opp)) by Th16, A1
.= ((/* S) . f) (*) ((/* S) . g) by A7, A6, A5, A3, A4, CAT_1:64 ; ::_thesis: verum
end;

definition
let C, D be Category;
mode Contravariant_Functor of C,D ->  Function of the carrier' of C, the carrier' of D means :Def9: :: OPPCAT_1:def 9
( ( for c being Object of C ex d being Object of D st it . (id c) = id d ) & ( for f being Morphism of C holds
( it . (id (dom f)) = id (cod (it . f)) & it . (id (cod f)) = id (dom (it . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
it . (g (*) f) = (it . f) (*) (it . g) ) );
existence
 ex b1 being Function of the carrier' of C, the carrier' of D st
( ( for c being Object of C ex d being Object of D st b1 . (id c) = id d ) & ( for f being Morphism of C holds
( b1 . (id (dom f)) = id (cod (b1 . f)) & b1 . (id (cod f)) = id (dom (b1 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b1 . (g (*) f) = (b1 . f) (*) (b1 . g) ) )
proof
set S = the Functor of C opp ,D;
take  /* the Functor of C opp ,D ; ::_thesis: ( ( for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d ) & ( for f being Morphism of C holds
( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) )
thus  for c being Object of C ex d being Object of D st (/* the Functor of C opp ,D) . (id c) = id d by Lm6; ::_thesis: ( ( for f being Morphism of C holds
( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ) )
thus  for f being Morphism of C holds
( (/* the Functor of C opp ,D) . (id (dom f)) = id (cod ((/* the Functor of C opp ,D) . f)) & (/* the Functor of C opp ,D) . (id (cod f)) = id (dom ((/* the Functor of C opp ,D) . f)) ) by Lm8; ::_thesis: for f, g being Morphism of C st dom g = cod f holds
(/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g)
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) )
assume A1: dom g = cod f ; ::_thesis: (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . 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 CAT_1:4, A1;
 ( Hom ((dom f),(cod f)) <> {} & Hom ((dom g),(cod g)) <> {} ) by CAT_1:2;
then  (/* the Functor of C opp ,D) . (gg (*) ff) = ((/* the Functor of C opp ,D) . ff) (*) ((/* the Functor of C opp ,D) . gg) by A1, Lm9;
hence  (/* the Functor of C opp ,D) . (g (*) f) = ((/* the Functor of C opp ,D) . f) (*) ((/* the Functor of C opp ,D) . g) ; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Contravariant_Functor OPPCAT_1:def_9_:_
 for C, D being Category
for b3 being Function of the carrier' of C, the carrier' of D holds
( b3 is Contravariant_Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b3 . (id c) = id d ) & ( for f being Morphism of C holds
( b3 . (id (dom f)) = id (cod (b3 . f)) & b3 . (id (cod f)) = id (dom (b3 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b3 . (g (*) f) = (b3 . f) (*) (b3 . g) ) ) );

theorem Th30: :: OPPCAT_1:30
for C, D being Category
for S being Contravariant_Functor of C,D
for c being Object of C
for d being Object of D st S . (id c) = id d holds
(Obj S) . c = d
proof
let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D
for c being Object of C
for d being Object of D st S . (id c) = id d holds
(Obj S) . c = d
let S be Contravariant_Functor of C,D; ::_thesis: for c being Object of C
for d being Object of D st S . (id c) = id d holds
(Obj S) . c = d
let c be Object of C; ::_thesis: for d being Object of D st S . (id c) = id d holds
(Obj S) . c = d
let d be Object of D; ::_thesis: ( S . (id c) = id d implies (Obj S) . c = d )
 for c being Object of C ex d being Object of D st S . (id c) = id d by Def9;
hence  ( S . (id c) = id d implies (Obj S) . c = d ) by CAT_1:66; ::_thesis: verum
end;

theorem Th31: :: OPPCAT_1:31
for C, D being Category
for S being Contravariant_Functor of C,D
for c being Object of C holds S . (id c) = id ((Obj S) . c)
proof
let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D
for c being Object of C holds S . (id c) = id ((Obj S) . c)
let S be Contravariant_Functor of C,D; ::_thesis: for c being Object of C holds S . (id c) = id ((Obj S) . c)
let c be Object of C; ::_thesis: S . (id c) = id ((Obj S) . c)
 ex d being Object of D st S . (id c) = id d by Def9;
hence  S . (id c) = id ((Obj S) . c) by Th30; ::_thesis: verum
end;

theorem Th32: :: OPPCAT_1:32
for C, D being Category
for S being Contravariant_Functor of C,D
for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
proof
let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D
for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
let S be Contravariant_Functor of C,D; ::_thesis: for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
let f be Morphism of C; ::_thesis: ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
 ( S . (id (dom f)) = id (cod (S . f)) & S . (id (cod f)) = id (dom (S . f)) ) by Def9;
hence  ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) ) by Th30; ::_thesis: verum
end;

theorem Th33: :: OPPCAT_1:33
for C, D being Category
for S being Contravariant_Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
dom (S . f) = cod (S . g)
proof
let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
dom (S . f) = cod (S . g)
let S be Contravariant_Functor of C,D; ::_thesis: for f, g being Morphism of C st dom g = cod f holds
dom (S . f) = cod (S . g)
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies dom (S . f) = cod (S . g) )
assume  dom g = cod f ; ::_thesis: dom (S . f) = cod (S . g)
hence  dom (S . f) = (Obj S) . (dom g) by Th32
.= cod (S . g) by Th32 ;
::_thesis: verum
end;

theorem Th34: :: OPPCAT_1:34
for C, B being Category
for S being Functor of C opp ,B holds /* S is Contravariant_Functor of C,B
proof
let C, B be Category; ::_thesis: for S being Functor of C opp ,B holds /* S is Contravariant_Functor of C,B
let S be Functor of C opp ,B; ::_thesis: /* S is Contravariant_Functor of C,B
thus  for c being Object of C ex d being Object of B st (/* S) . (id c) = id d by Lm6; :: according to OPPCAT_1:def_9 ::_thesis: ( ( for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ) )
thus  for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) & (/* S) . (id (cod f)) = id (dom ((/* S) . f)) ) by Lm8; ::_thesis: for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) )
assume A1: dom g = cod f ; ::_thesis: (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . 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 CAT_1:4, A1;
 ( 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  (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g) ; ::_thesis: verum
end;

theorem Th35: :: OPPCAT_1:35
for C, B, D being Category
for S1 being Contravariant_Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D
proof
let C, B, D be Category; ::_thesis: for S1 being Contravariant_Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D
let S1 be Contravariant_Functor of C,B; ::_thesis: for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D
let S2 be Contravariant_Functor of B,D; ::_thesis: S2 * S1 is Functor of C,D
set T = S2 * S1;
now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_D_st_(S2_*_S1)_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_
(_(S2_*_S1)_._(id_(dom_f))_=_id_(dom_((S2_*_S1)_._f))_&_(S2_*_S1)_._(id_(cod_f))_=_id_(cod_((S2_*_S1)_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_
(S2_*_S1)_._(g_(*)_f)_=_((S2_*_S1)_._g)_(*)_((S2_*_S1)_._f)_)_)
thus  for c being Object of C ex d being Object of D st (S2 * S1) . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds
( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) ) )
proof
let c be Object of C; ::_thesis: ex d being Object of D st (S2 * S1) . (id c) = id d
consider b being Object of B such that
A1: S1 . (id c) = id b by Def9;
consider d being Object of D such that
A2: S2 . (id b) = id d by Def9;
take  d ; ::_thesis: (S2 * S1) . (id c) = id d
thus  (S2 * S1) . (id c) = id d by A1, A2, FUNCT_2:15; ::_thesis: verum
end;
thus  for f being Morphism of C holds
( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
(S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f)
proof
let f be Morphism of C; ::_thesis: ( (S2 * S1) . (id (dom f)) = id (dom ((S2 * S1) . f)) & (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f)) )
thus (S2 * S1) . (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 ((S2 * S1) . f)) by FUNCT_2:15 ; ::_thesis: (S2 * S1) . (id (cod f)) = id (cod ((S2 * S1) . f))
thus (S2 * S1) . (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 ((S2 * S1) . f)) by FUNCT_2:15 ; ::_thesis: verum
end;
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f) )
assume A3: dom g = cod f ; ::_thesis: (S2 * S1) . (g (*) f) = ((S2 * S1) . g) (*) ((S2 * S1) . f)
then A4: cod (S1 . g) = dom (S1 . f) by Th33;
thus (S2 * S1) . (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
.= ((S2 * S1) . g) (*) (S2 . (S1 . f)) by FUNCT_2:15
.= ((S2 * S1) . g) (*) ((S2 * S1) . f) by FUNCT_2:15 ; ::_thesis: verum
end;
hence  S2 * S1 is Functor of C,D by CAT_1:61; ::_thesis: verum
end;

Lm10:  for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj S) . (c opp))
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 Th20
.= id ((Obj S) . (c opp)) by Th31 ; ::_thesis: verum
end;

theorem Th36: :: OPPCAT_1:36
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
let c be Object of C; ::_thesis: (Obj (/* S)) . c = (Obj S) . (c opp)
A1: now__::_thesis:_for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d
let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d
 (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm10;
hence  ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum
end;
 (/* S) . (id c) = id ((Obj S) . (c opp)) by Lm10;
hence  (Obj (/* S)) . c = (Obj S) . (c opp) by A1, CAT_1:66; ::_thesis: verum
end;

theorem :: OPPCAT_1:37
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B
for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
let c be Object of (C opp); ::_thesis: (Obj (/* S)) . (opp c) = (Obj S) . c
thus (Obj (/* S)) . (opp c) = (Obj S) . ((opp c) opp) by Th36
.= (Obj S) . c ; ::_thesis: verum
end;

Lm11:  for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
let S be Contravariant_Functor of C opp ,B; ::_thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
let c be Object of C; ::_thesis: (/* S) . (id c) = id ((Obj (/* S)) . 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 Th20
.= id ((Obj S) . (c opp)) by Th31
.= id ((Obj (/* S)) . c) by Th36 ; ::_thesis: verum
end;

Lm12:  for C, B being Category
for S being Contravariant_Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
let S be Contravariant_Functor of C opp ,B; ::_thesis: for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
let f be Morphism of C; ::_thesis: ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
A1: (Obj (/* S)) . (cod f) = (Obj S) . ((cod f) opp) by Th36
.= (Obj S) . (dom (f opp))
.= cod (S . (f opp)) by Th32 ;
(Obj (/* S)) . (dom f) = (Obj S) . ((dom f) opp) by Th36
.= (Obj S) . (cod (f opp))
.= dom (S . (f opp)) by Th32 ;
hence  ( (Obj (/* S)) . (dom f) = dom ((/* S) . f) & (Obj (/* S)) . (cod f) = cod ((/* S) . f) ) by A1, Def8; ::_thesis: verum
end;

theorem :: OPPCAT_1:38
for C, B being Category
for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B
let S be Contravariant_Functor of C opp ,B; ::_thesis: /* S is Functor of C,B
now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_
(_(/*_S)_._(id_(dom_f))_=_id_(dom_((/*_S)_._f))_&_(/*_S)_._(id_(cod_f))_=_id_(cod_((/*_S)_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_
(/*_S)_._(g_(*)_f)_=_((/*_S)_._g)_(*)_((/*_S)_._f)_)_)
thus  for c being Object of C ex d being Object of B st (/* S) . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (dom ((/* S) . f)) & (/* S) . (id (cod f)) = id (cod ((/* S) . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . f) ) )
proof
let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d
 (/* S) . (id c) = id ((Obj (/* S)) . c) by Lm11;
hence  ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum
end;
thus  for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (dom ((/* S) . f)) & (/* S) . (id (cod f)) = id (cod ((/* S) . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
(/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . f)
proof
let f be Morphism of C; ::_thesis: ( (/* S) . (id (dom f)) = id (dom ((/* S) . f)) & (/* S) . (id (cod f)) = id (cod ((/* S) . f)) )
thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm11
.= id (dom ((/* S) . f)) by Lm12 ; ::_thesis: (/* S) . (id (cod f)) = id (cod ((/* S) . f))
thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm11
.= id (cod ((/* S) . f)) by Lm12 ; ::_thesis: verum
end;
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . f) )
assume A1: dom g = cod f ; ::_thesis: (/* S) . (g (*) f) = ((/* S) . g) (*) ((/* S) . 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 CAT_1:4, A1;
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, Th16
.= (S . (g opp)) (*) (S . (f opp)) by A1, A2, Def9
.= ((/* S) . g) (*) (S . (f opp)) by Def8
.= ((/* S) . g) (*) ((/* S) . f) by Def8 ; ::_thesis: verum
end;
hence  /* S is Functor of C,B by CAT_1:61; ::_thesis: verum
end;

definition
let C, B be Category;
let S be Function of the carrier' of C, the carrier' of B;
func *' S ->  Function of the carrier' of (C opp), the carrier' of B means :Def10: :: OPPCAT_1:def 10
 for f being Morphism of (C opp) holds it . f = S . (opp f);
existence
 ex b1 being Function of the carrier' of (C opp), the carrier' of B st
for f being Morphism of (C opp) holds b1 . f = S . (opp f)
proof
deffunc H1( Morphism of (C opp)) ->  Element of the carrier' of B = S . (opp $1);
thus  ex F being Function of the carrier' of (C opp), the carrier' of B st
for f being Morphism of (C opp) holds F . f = H1(f) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier' of (C opp), the carrier' of B st ( for f being Morphism of (C opp) holds b1 . f = S . (opp f) ) & ( for f being Morphism of (C opp) holds b2 . f = S . (opp f) ) holds
b1 = b2
proof
let T1, T2 be Function of the carrier' of (C opp), the carrier' of B; ::_thesis: ( ( for f being Morphism of (C opp) holds T1 . f = S . (opp f) ) & ( for f being Morphism of (C opp) holds T2 . f = S . (opp f) ) implies T1 = T2 )
assume that
A1: for f being Morphism of (C opp) holds T1 . f = S . (opp f) and
A2: for f being Morphism of (C opp) holds T2 . f = S . (opp f) ; ::_thesis: T1 = T2
now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_T1_._f_=_T2_._f
let f be Morphism of (C opp); ::_thesis: T1 . f = T2 . f
thus T1 . f = S . (opp f) by A1
.= T2 . f by A2 ; ::_thesis: verum
end;
hence  T1 = T2 by FUNCT_2:63; ::_thesis: verum
end;
funcS *'  ->  Function of the carrier' of C, the carrier' of (B opp) means :Def11: :: OPPCAT_1:def 11
 for f being Morphism of C holds it . f = (S . f) opp ;
existence
 ex b1 being Function of the carrier' of C, the carrier' of (B opp) st
for f being Morphism of C holds b1 . f = (S . f) opp
proof
deffunc H1( Morphism of C) ->  Morphism of (B opp) = (S . $1) opp ;
thus  ex F being Function of the carrier' of C, the carrier' of (B opp) st
for f being Morphism of C holds F . f = H1(f) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the carrier' of C, the carrier' of (B opp) st ( for f being Morphism of C holds b1 . f = (S . f) opp ) & ( for f being Morphism of C holds b2 . f = (S . f) opp ) holds
b1 = b2
proof
let T1, T2 be Function of the carrier' of C, the carrier' of (B opp); ::_thesis: ( ( for f being Morphism of C holds T1 . f = (S . f) opp ) & ( for f being Morphism of C holds T2 . f = (S . f) opp ) implies T1 = T2 )
assume that
A3: for f being Morphism of C holds T1 . f = (S . f) opp and
A4: for f being Morphism of C holds T2 . f = (S . f) opp ; ::_thesis: T1 = T2
now__::_thesis:_for_f_being_Morphism_of_C_holds_T1_._f_=_T2_._f
let f be Morphism of C; ::_thesis: T1 . f = T2 . f
thus T1 . f = (S . f) opp by A3
.= T2 . f by A4 ; ::_thesis: verum
end;
hence  T1 = T2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines *' OPPCAT_1:def_10_:_
 for C, B being Category
for S being Function of the carrier' of C, the carrier' of B
for b4 being Function of the carrier' of (C opp), the carrier' of B holds
( b4 = *' S iff for f being Morphism of (C opp) holds b4 . f = S . (opp f) );

:: deftheorem Def11 defines *' OPPCAT_1:def_11_:_
 for C, B being Category
for S being Function of the carrier' of C, the carrier' of B
for b4 being Function of the carrier' of C, the carrier' of (B opp) holds
( b4 = S *' iff for f being Morphism of C holds b4 . f = (S . f) opp );

theorem :: OPPCAT_1:39
for C, B being Category
for S being Function of the carrier' of C, the carrier' of B
for f being Morphism of C holds (*' S) . (f opp) = S . f
proof
let C, B be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of B
for f being Morphism of C holds (*' S) . (f opp) = S . f
let S be Function of the carrier' of C, the carrier' of B; ::_thesis: for f being Morphism of C holds (*' S) . (f opp) = S . f
let f be Morphism of C; ::_thesis: (*' S) . (f opp) = S . f
thus (*' S) . (f opp) = S . (opp (f opp)) by Def10
.= S . f ; ::_thesis: verum
end;

Lm13:  for C, B being Category
for S being Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
let S be Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj S) . (opp c))
thus (*' S) . (id c) = S . (opp (id c)) by Def10
.= S . (id (opp c)) by Th21
.= id ((Obj S) . (opp c)) by CAT_1:68 ; ::_thesis: verum
end;

theorem Th40: :: OPPCAT_1:40
for C, B being Category
for S being Functor of C,B
for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
let S be Functor of C,B; ::_thesis: for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
let c be Object of (C opp); ::_thesis: (Obj (*' S)) . c = (Obj S) . (opp c)
now__::_thesis:_(_(*'_S)_._(id_c)_=_id_((Obj_S)_._(opp_c))_&_(_for_c_being_Object_of_(C_opp)_ex_d_being_Object_of_B_st_(*'_S)_._(id_c)_=_id_d_)_)
thus  (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm13; ::_thesis: for c being Object of (C opp) ex d being Object of B st (*' S) . (id c) = id d
let c be Object of (C opp); ::_thesis: ex d being Object of B st (*' S) . (id c) = id d
 (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm13;
hence  ex d being Object of B st (*' S) . (id c) = id d ; ::_thesis: verum
end;
hence  (Obj (*' S)) . c = (Obj S) . (opp c) by CAT_1:66; ::_thesis: verum
end;

theorem :: OPPCAT_1:41
for C, B being Category
for S being Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
let S be Functor of C,B; ::_thesis: for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
let c be Object of C; ::_thesis: (Obj (*' S)) . (c opp) = (Obj S) . c
thus (Obj (*' S)) . (c opp) = (Obj S) . (opp (c opp)) by Th40
.= (Obj S) . c ; ::_thesis: verum
end;

Lm14:  for C, B being Category
for S being Functor of C,B
for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
let S be Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
let c be Object of C; ::_thesis: (S *') . (id c) = id (((Obj S) . c) opp)
A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ;
thus (S *') . (id c) = (S . (id c)) opp by Def11
.= (id ((Obj S) . c)) opp by CAT_1:68
.= (id ((Obj S) . c)) opp by Def6, A1
.= id (((Obj S) . c) opp) by Th20 ; ::_thesis: verum
end;

theorem Th42: :: OPPCAT_1:42
for C, B being Category
for S being Functor of C,B
for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
let S be Functor of C,B; ::_thesis: for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
let c be Object of C; ::_thesis: (Obj (S *')) . c = ((Obj S) . c) opp
now__::_thesis:_(_(S_*')_._(id_c)_=_id_(((Obj_S)_._c)_opp)_&_(_for_c_being_Object_of_C_ex_d_being_Object_of_(B_opp)_st_(S_*')_._(id_c)_=_id_d_)_)
thus  (S *') . (id c) = id (((Obj S) . c) opp) by Lm14; ::_thesis: for c being Object of C ex d being Object of (B opp) st (S *') . (id c) = id d
let c be Object of C; ::_thesis: ex d being Object of (B opp) st (S *') . (id c) = id d
 (S *') . (id c) = id (((Obj S) . c) opp) by Lm14;
hence  ex d being Object of (B opp) st (S *') . (id c) = id d ; ::_thesis: verum
end;
hence  (Obj (S *')) . c = ((Obj S) . c) opp by CAT_1:66; ::_thesis: verum
end;

Lm15:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj S) . (opp c))
thus (*' S) . (id c) = S . (opp (id c)) by Def10
.= S . (id (opp c)) by Th21
.= id ((Obj S) . (opp c)) by Th31 ; ::_thesis: verum
end;

theorem Th43: :: OPPCAT_1:43
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
let c be Object of (C opp); ::_thesis: (Obj (*' S)) . c = (Obj S) . (opp c)
now__::_thesis:_(_(*'_S)_._(id_c)_=_id_((Obj_S)_._(opp_c))_&_(_for_c_being_Object_of_(C_opp)_ex_d_being_Object_of_B_st_(*'_S)_._(id_c)_=_id_d_)_)
thus  (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm15; ::_thesis: for c being Object of (C opp) ex d being Object of B st (*' S) . (id c) = id d
let c be Object of (C opp); ::_thesis: ex d being Object of B st (*' S) . (id c) = id d
 (*' S) . (id c) = id ((Obj S) . (opp c)) by Lm15;
hence  ex d being Object of B st (*' S) . (id c) = id d ; ::_thesis: verum
end;
hence  (Obj (*' S)) . c = (Obj S) . (opp c) by CAT_1:66; ::_thesis: verum
end;

theorem :: OPPCAT_1:44
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
let c be Object of C; ::_thesis: (Obj (*' S)) . (c opp) = (Obj S) . c
thus (Obj (*' S)) . (c opp) = (Obj S) . (opp (c opp)) by Th43
.= (Obj S) . c ; ::_thesis: verum
end;

Lm16:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
let c be Object of C; ::_thesis: (S *') . (id c) = id (((Obj S) . c) opp)
A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ;
thus (S *') . (id c) = (S . (id c)) opp by Def11
.= (id ((Obj S) . c)) opp by Th31
.= (id ((Obj S) . c)) opp by Def6, A1
.= id (((Obj S) . c) opp) by Th20 ; ::_thesis: verum
end;

theorem Th45: :: OPPCAT_1:45
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
let c be Object of C; ::_thesis: (Obj (S *')) . c = ((Obj S) . c) opp
now__::_thesis:_(_(S_*')_._(id_c)_=_id_(((Obj_S)_._c)_opp)_&_(_for_c_being_Object_of_C_ex_d_being_Object_of_(B_opp)_st_(S_*')_._(id_c)_=_id_d_)_)
thus  (S *') . (id c) = id (((Obj S) . c) opp) by Lm16; ::_thesis: for c being Object of C ex d being Object of (B opp) st (S *') . (id c) = id d
let c be Object of C; ::_thesis: ex d being Object of (B opp) st (S *') . (id c) = id d
 (S *') . (id c) = id (((Obj S) . c) opp) by Lm16;
hence  ex d being Object of (B opp) st (S *') . (id c) = id d ; ::_thesis: verum
end;
hence  (Obj (S *')) . c = ((Obj S) . c) opp by CAT_1:66; ::_thesis: verum
end;

Lm17:  for C, D being Category
for F being Function of the carrier' of C, the carrier' of D
for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp
proof
let C, D be Category; ::_thesis: for F being Function of the carrier' of C, the carrier' of D
for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp
let F be Function of the carrier' of C, the carrier' of D; ::_thesis: for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp
let f be Morphism of (C opp); ::_thesis: ((*' F) *') . f = (F . (opp f)) opp
thus ((*' F) *') . f = ((*' F) . f) opp by Def11
.= (F . (opp f)) opp by Def10 ; ::_thesis: verum
end;

theorem Th46: :: OPPCAT_1:46
for C, D being Category
for F being Function of the carrier' of C, the carrier' of D
for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp
proof
let C, D be Category; ::_thesis: for F being Function of the carrier' of C, the carrier' of D
for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp
let F be Function of the carrier' of C, the carrier' of D; ::_thesis: for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp
let f be Morphism of C; ::_thesis: ((*' F) *') . (f opp) = (F . f) opp
thus ((*' F) *') . (f opp) = (F . (opp (f opp))) opp by Lm17
.= (F . f) opp ; ::_thesis: verum
end;

theorem Th47: :: OPPCAT_1:47
for C, D being Category
for S being Function of the carrier' of C, the carrier' of D holds /* (*' S) = S
proof
let C, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds /* (*' S) = S
let S be Function of the carrier' of C, the carrier' of D; ::_thesis: /* (*' S) = S
now__::_thesis:_for_f_being_Morphism_of_C_holds_(/*_(*'_S))_._f_=_S_._f
let f be Morphism of C; ::_thesis: (/* (*' S)) . f = S . f
thus (/* (*' S)) . f = (*' S) . (f opp) by Def8
.= S . (opp (f opp)) by Def10
.= S . f ; ::_thesis: verum
end;
hence  /* (*' S) = S by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:48
for C, D being Category
for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S
proof
let C, D be Category; ::_thesis: for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S
let S be Function of the carrier' of (C opp), the carrier' of D; ::_thesis: *' (/* S) = S
now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_(*'_(/*_S))_._f_=_S_._f
let f be Morphism of (C opp); ::_thesis: (*' (/* S)) . f = S . f
thus (*' (/* S)) . f = (/* S) . (opp f) by Def10
.= S . ((opp f) opp) by Def8
.= S . f ; ::_thesis: verum
end;
hence  *' (/* S) = S by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:49
for C, D being Category
for S being Function of the carrier' of C, the carrier' of D holds (*' S) *' = *' (S *')
proof
let C, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds (*' S) *' = *' (S *')
let S be Function of the carrier' of C, the carrier' of D; ::_thesis: (*' S) *' = *' (S *')
now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_((*'_S)_*')_._f_=_(*'_(S_*'))_._f
let f be Morphism of (C opp); ::_thesis: ((*' S) *') . f = (*' (S *')) . f
thus ((*' S) *') . f = ((*' S) . f) opp by Def11
.= (S . (opp f)) opp by Def10
.= (S *') . (opp f) by Def11
.= (*' (S *')) . f by Def10 ; ::_thesis: verum
end;
hence  (*' S) *' = *' (S *') by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:50
for C being Category
for D being strict Category
for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S
proof
let C be Category; ::_thesis: for D being strict Category
for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S
let D be strict Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S
let S be Function of the carrier' of C, the carrier' of D; ::_thesis: (S *') *' = S
now__::_thesis:_(_(D_opp)_opp_=_D_&_(_for_f_being_Morphism_of_C_holds_((S_*')_*')_._f_=_S_._f_)_)
thus  (D opp) opp = D by FUNCT_4:53; ::_thesis: for f being Morphism of C holds ((S *') *') . f = S . f
let f be Morphism of C; ::_thesis: ((S *') *') . f = S . f
thus ((S *') *') . f = ((S *') . f) opp by Def11
.= ((S . f) opp) opp by Def11
.= S . f ; ::_thesis: verum
end;
hence  (S *') *' = S by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:51
for D being Category
for C being strict Category
for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S
proof
let D be Category; ::_thesis: for C being strict Category
for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S
let C be strict Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S
let S be Function of the carrier' of C, the carrier' of D; ::_thesis: *' (*' S) = S
now__::_thesis:_(_(C_opp)_opp_=_C_&_(_for_f_being_Morphism_of_((C_opp)_opp)_holds_(*'_(*'_S))_._f_=_S_._f_)_)
thus  (C opp) opp = C by FUNCT_4:53; ::_thesis: for f being Morphism of ((C opp) opp) holds (*' (*' S)) . f = S . f
let f be Morphism of ((C opp) opp); ::_thesis: (*' (*' S)) . f = S . f
thus (*' (*' S)) . f = (*' S) . (opp f) by Def10
.= S . (opp (opp f)) by Def10
.= S . f ; ::_thesis: verum
end;
hence  *' (*' S) = S by FUNCT_2:63; ::_thesis: verum
end;

Lm18:  for C, B, D being Category
for S being Function of the carrier' of (C opp), the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S)
proof
let C, B, D be Category; ::_thesis: for S being Function of the carrier' of (C opp), the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S)
let S be Function of the carrier' of (C opp), the carrier' of B; ::_thesis: for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S)
let T be Function of the carrier' of B, the carrier' of D; ::_thesis: /* (T * S) = T * (/* S)
now__::_thesis:_for_f_being_Morphism_of_C_holds_(/*_(T_*_S))_._f_=_(T_*_(/*_S))_._f
let f be Morphism of C; ::_thesis: (/* (T * S)) . f = (T * (/* S)) . f
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 ; ::_thesis: verum
end;
hence  /* (T * S) = T * (/* S) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:52
for C, B, D being Category
for S being Function of the carrier' of C, the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S)
proof
let C, B, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S)
let S be Function of the carrier' of C, the carrier' of B; ::_thesis: for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S)
let T be Function of the carrier' of B, the carrier' of D; ::_thesis: *' (T * S) = T * (*' S)
now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_(*'_(T_*_S))_._f_=_(T_*_(*'_S))_._f
let f be Morphism of (C opp); ::_thesis: (*' (T * S)) . f = (T * (*' S)) . f
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 ; ::_thesis: verum
end;
hence  *' (T * S) = T * (*' S) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:53
for C, B, D being Category
for S being Function of the carrier' of C, the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds (T * S) *' = (T *') * S
proof
let C, B, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds (T * S) *' = (T *') * S
let S be Function of the carrier' of C, the carrier' of B; ::_thesis: for T being Function of the carrier' of B, the carrier' of D holds (T * S) *' = (T *') * S
let T be Function of the carrier' of B, the carrier' of D; ::_thesis: (T * S) *' = (T *') * S
now__::_thesis:_for_f_being_Morphism_of_C_holds_((T_*_S)_*')_._f_=_((T_*')_*_S)_._f
let f be Morphism of C; ::_thesis: ((T * S) *') . f = ((T *') * S) . f
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 ; ::_thesis: verum
end;
hence  (T * S) *' = (T *') * S by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:54
for C, B, D being Category
for F1 being Function of the carrier' of C, the carrier' of B
for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')
proof
let C, B, D be Category; ::_thesis: for F1 being Function of the carrier' of C, the carrier' of B
for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')
let F1 be Function of the carrier' of C, the carrier' of B; ::_thesis: for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')
let F2 be Function of the carrier' of B, the carrier' of D; ::_thesis: (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')
now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_((*'_(F2_*_F1))_*')_._f_=_(((*'_F2)_*')_*_((*'_F1)_*'))_._f
let f be Morphism of (C opp); ::_thesis: ((*' (F2 * F1)) *') . f = (((*' F2) *') * ((*' F1) *')) . f
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 Th46
.= ((*' F2) *') . (((*' F1) *') . f) by Lm17
.= (((*' F2) *') * ((*' F1) *')) . f by FUNCT_2:15 ; ::_thesis: verum
end;
hence  (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *') by FUNCT_2:63; ::_thesis: verum
end;

Lm19:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj (*' S)) . c)
thus (*' S) . (id c) = S . (opp (id c)) by Def10
.= S . (id (opp c)) by Th21
.= id ((Obj S) . (opp c)) by Th31
.= id ((Obj (*' S)) . c) by Th43 ; ::_thesis: verum
end;

Lm20:  for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
let S be Contravariant_Functor of C,B; ::_thesis: for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
let f be Morphism of (C opp); ::_thesis: ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
A1: (Obj (*' S)) . (cod f) = (Obj S) . (opp (cod f)) by Th43
.= (Obj S) . (dom (opp f))
.= cod (S . (opp f)) by Th32 ;
(Obj (*' S)) . (dom f) = (Obj S) . (opp (dom f)) by Th43
.= (Obj S) . (cod (opp f))
.= dom (S . (opp f)) by Th32 ;
hence  ( (Obj (*' S)) . (dom f) = dom ((*' S) . f) & (Obj (*' S)) . (cod f) = cod ((*' S) . f) ) by A1, Def10; ::_thesis: verum
end;

theorem Th55: :: OPPCAT_1:55
for C, D being Category
for S being Contravariant_Functor of C,D holds *' S is Functor of C opp ,D
proof
let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D holds *' S is Functor of C opp ,D
let S be Contravariant_Functor of C,D; ::_thesis: *' S is Functor of C opp ,D
now__::_thesis:_(_(_for_c_being_Object_of_(C_opp)_ex_d_being_Object_of_D_st_(*'_S)_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_(C_opp)_holds_
(_(*'_S)_._(id_(dom_f))_=_id_(dom_((*'_S)_._f))_&_(*'_S)_._(id_(cod_f))_=_id_(cod_((*'_S)_._f))_)_)_&_(_for_f,_g_being_Morphism_of_(C_opp)_st_dom_g_=_cod_f_holds_
(*'_S)_._(g_(*)_f)_=_((*'_S)_._g)_(*)_((*'_S)_._f)_)_)
thus  for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d ::_thesis: ( ( for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) ) )
proof
let c be Object of (C opp); ::_thesis: ex d being Object of D st (*' S) . (id c) = id d
 (*' S) . (id c) = id ((Obj (*' S)) . c) by Lm19;
hence  ex d being Object of D st (*' S) . (id c) = id d ; ::_thesis: verum
end;
thus  for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) ) ::_thesis: for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f)
proof
let f be Morphism of (C opp); ::_thesis: ( (*' S) . (id (dom f)) = id (dom ((*' S) . f)) & (*' S) . (id (cod f)) = id (cod ((*' S) . f)) )
thus (*' S) . (id (dom f)) = id ((Obj (*' S)) . (dom f)) by Lm19
.= id (dom ((*' S) . f)) by Lm20 ; ::_thesis: (*' S) . (id (cod f)) = id (cod ((*' S) . f))
thus (*' S) . (id (cod f)) = id ((Obj (*' S)) . (cod f)) by Lm19
.= id (cod ((*' S) . f)) by Lm20 ; ::_thesis: verum
end;
let f, g be Morphism of (C opp); ::_thesis: ( dom g = cod f implies (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . f) )
assume A1: dom g = cod f ; ::_thesis: (*' S) . (g (*) f) = ((*' S) . g) (*) ((*' S) . 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, Th18
.= (S . (opp g)) (*) (S . (opp f)) by A1, A2, Def9
.= ((*' S) . g) (*) (S . (opp f)) by Def10
.= ((*' S) . g) (*) ((*' S) . f) by Def10 ; ::_thesis: verum
end;
hence  *' S is Functor of C opp ,D by CAT_1:61; ::_thesis: verum
end;

Lm21:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
let S be Contravariant_Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
let c be Object of C; ::_thesis: (S *') . (id c) = id ((Obj (S *')) . c)
A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ;
thus (S *') . (id c) = (S . (id c)) opp by Def11
.= (id ((Obj S) . c)) opp by Th31
.= (id ((Obj S) . c)) opp by Def6, A1
.= id (((Obj S) . c) opp) by Th20
.= id ((Obj (S *')) . c) by Th45 ; ::_thesis: verum
end;

Lm22:  for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of C holds
( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) )
proof
let C, B be Category; ::_thesis: for S being Contravariant_Functor of C,B
for f being Morphism of C holds
( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) )
let S be Contravariant_Functor of C,B; ::_thesis: for f being Morphism of C holds
( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) )
let f be Morphism of C; ::_thesis: ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) )
A1: (Obj (S *')) . (cod f) = ((Obj S) . (cod f)) opp by Th45
.= (dom (S . f)) opp by Th32
.= cod ((S . f) opp) ;
(Obj (S *')) . (dom f) = ((Obj S) . (dom f)) opp by Th45
.= (cod (S . f)) opp by Th32
.= dom ((S . f) opp) ;
hence  ( (Obj (S *')) . (dom f) = dom ((S *') . f) & (Obj (S *')) . (cod f) = cod ((S *') . f) ) by A1, Def11; ::_thesis: verum
end;

theorem Th56: :: OPPCAT_1:56
for C, D being Category
for S being Contravariant_Functor of C,D holds S *' is Functor of C,D opp
proof
let C, D be Category; ::_thesis: for S being Contravariant_Functor of C,D holds S *' is Functor of C,D opp
let S be Contravariant_Functor of C,D; ::_thesis: S *' is Functor of C,D opp
now__::_thesis:_(_(_for_c_being_Object_of_C_ex_d_being_Object_of_(D_opp)_st_(S_*')_._(id_c)_=_id_d_)_&_(_for_f_being_Morphism_of_C_holds_
(_(S_*')_._(id_(dom_f))_=_id_(dom_((S_*')_._f))_&_(S_*')_._(id_(cod_f))_=_id_(cod_((S_*')_._f))_)_)_&_(_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_
(S_*')_._(g_(*)_f)_=_((S_*')_._g)_(*)_((S_*')_._f)_)_)
thus  for c being Object of C ex d being Object of (D opp) st (S *') . (id c) = id d ::_thesis: ( ( for f being Morphism of C holds
( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) ) )
proof
let c be Object of C; ::_thesis: ex d being Object of (D opp) st (S *') . (id c) = id d
 (S *') . (id c) = id (((Obj S) . c) opp) by Lm16;
hence  ex d being Object of (D opp) st (S *') . (id c) = id d ; ::_thesis: verum
end;
thus  for f being Morphism of C holds
( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
(S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f)
proof
let f be Morphism of C; ::_thesis: ( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) )
thus (S *') . (id (dom f)) = id ((Obj (S *')) . (dom f)) by Lm21
.= id (dom ((S *') . f)) by Lm22 ; ::_thesis: (S *') . (id (cod f)) = id (cod ((S *') . f))
thus (S *') . (id (cod f)) = id ((Obj (S *')) . (cod f)) by Lm21
.= id (cod ((S *') . f)) by Lm22 ; ::_thesis: verum
end;
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) )
assume A1: dom g = cod f ; ::_thesis: (S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f)
then A2: dom (S . f) = cod (S . g) by Th33;
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, Th16
.= ((S *') . g) (*) ((S . f) opp) by Def11, A4, A5
.= ((S *') . g) (*) ((S *') . f) by Def11 ; ::_thesis: verum
end;
hence  S *' is Functor of C,D opp by CAT_1:61; ::_thesis: verum
end;

Lm23:  for C, B being Category
for S being Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
let S be Functor of C,B; ::_thesis: for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
let c be Object of (C opp); ::_thesis: (*' S) . (id c) = id ((Obj (*' S)) . c)
thus (*' S) . (id c) = S . (opp (id c)) by Def10
.= S . (id (opp c)) by Th21
.= id ((Obj S) . (opp c)) by CAT_1:68
.= id ((Obj (*' S)) . c) by Th40 ; ::_thesis: verum
end;

Lm24:  for C, B being Category
for S being Functor of C,B
for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) )
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) )
let S be Functor of C,B; ::_thesis: for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) )
let f be Morphism of (C opp); ::_thesis: ( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) )
A1: (Obj (*' S)) . (cod f) = (Obj S) . (opp (cod f)) by Th40
.= (Obj S) . (dom (opp f))
.= dom (S . (opp f)) by CAT_1:69 ;
(Obj (*' S)) . (dom f) = (Obj S) . (opp (dom f)) by Th40
.= (Obj S) . (cod (opp f))
.= cod (S . (opp f)) by CAT_1:69 ;
hence  ( (Obj (*' S)) . (dom f) = cod ((*' S) . f) & (Obj (*' S)) . (cod f) = dom ((*' S) . f) ) by A1, Def10; ::_thesis: verum
end;

theorem Th57: :: OPPCAT_1:57
for C, D being Category
for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D
proof
let C, D be Category; ::_thesis: for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D
let S be Functor of C,D; ::_thesis: *' S is Contravariant_Functor of C opp ,D
thus  for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d :: according to OPPCAT_1:def_9 ::_thesis: ( ( for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) ) )
proof
let c be Object of (C opp); ::_thesis: ex d being Object of D st (*' S) . (id c) = id d
 (*' S) . (id c) = id ((Obj (*' S)) . c) by Lm23;
hence  ex d being Object of D st (*' S) . (id c) = id d ; ::_thesis: verum
end;
thus  for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) ::_thesis: for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g)
proof
let f be Morphism of (C opp); ::_thesis: ( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) )
thus (*' S) . (id (dom f)) = id ((Obj (*' S)) . (dom f)) by Lm23
.= id (cod ((*' S) . f)) by Lm24 ; ::_thesis: (*' S) . (id (cod f)) = id (dom ((*' S) . f))
thus (*' S) . (id (cod f)) = id ((Obj (*' S)) . (cod f)) by Lm23
.= id (dom ((*' S) . f)) by Lm24 ; ::_thesis: verum
end;
let f, g be Morphism of (C opp); ::_thesis: ( dom g = cod f implies (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) )
assume A1: dom g = cod f ; ::_thesis: (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g)
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, Th18
.= (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 ; ::_thesis: verum
end;

Lm25:  for C, B being Category
for S being Functor of C,B
for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
let S be Functor of C,B; ::_thesis: for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
let c be Object of C; ::_thesis: (S *') . (id c) = id ((Obj (S *')) . c)
A1: Hom (((Obj S) . c),((Obj S) . c)) <> {} ;
thus (S *') . (id c) = (S . (id c)) opp by Def11
.= (id ((Obj S) . c)) opp by CAT_1:68
.= (id ((Obj S) . c)) opp by Def6, A1
.= id (((Obj S) . c) opp) by Th20
.= id ((Obj (S *')) . c) by Th42 ; ::_thesis: verum
end;

Lm26:  for C, B being Category
for S being Functor of C,B
for f being Morphism of C holds
( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) )
proof
let C, B be Category; ::_thesis: for S being Functor of C,B
for f being Morphism of C holds
( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) )
let S be Functor of C,B; ::_thesis: for f being Morphism of C holds
( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) )
let f be Morphism of C; ::_thesis: ( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) )
A1: (Obj (S *')) . (cod f) = ((Obj S) . (cod f)) opp by Th42
.= (cod (S . f)) opp by CAT_1:69
.= dom ((S . f) opp) ;
(Obj (S *')) . (dom f) = ((Obj S) . (dom f)) opp by Th42
.= (dom (S . f)) opp by CAT_1:69
.= cod ((S . f) opp) ;
hence  ( (Obj (S *')) . (dom f) = cod ((S *') . f) & (Obj (S *')) . (cod f) = dom ((S *') . f) ) by A1, Def11; ::_thesis: verum
end;

theorem Th58: :: OPPCAT_1:58
for C, D being Category
for S being Functor of C,D holds S *' is Contravariant_Functor of C,D opp
proof
let C, D be Category; ::_thesis: for S being Functor of C,D holds S *' is Contravariant_Functor of C,D opp
let S be Functor of C,D; ::_thesis: S *' is Contravariant_Functor of C,D opp
thus  for c being Object of C ex d being Object of (D opp) st (S *') . (id c) = id d :: according to OPPCAT_1:def_9 ::_thesis: ( ( for f being Morphism of C holds
( (S *') . (id (dom f)) = id (cod ((S *') . f)) & (S *') . (id (cod f)) = id (dom ((S *') . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g) ) )
proof
let c be Object of C; ::_thesis: ex d being Object of (D opp) st (S *') . (id c) = id d
 (S *') . (id c) = id ((Obj (S *')) . c) by Lm25;
hence  ex d being Object of (D opp) st (S *') . (id c) = id d ; ::_thesis: verum
end;
thus  for f being Morphism of C holds
( (S *') . (id (dom f)) = id (cod ((S *') . f)) & (S *') . (id (cod f)) = id (dom ((S *') . f)) ) ::_thesis: for f, g being Morphism of C st dom g = cod f holds
(S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g)
proof
let f be Morphism of C; ::_thesis: ( (S *') . (id (dom f)) = id (cod ((S *') . f)) & (S *') . (id (cod f)) = id (dom ((S *') . f)) )
thus (S *') . (id (dom f)) = id ((Obj (S *')) . (dom f)) by Lm25
.= id (cod ((S *') . f)) by Lm26 ; ::_thesis: (S *') . (id (cod f)) = id (dom ((S *') . f))
thus (S *') . (id (cod f)) = id ((Obj (S *')) . (cod f)) by Lm25
.= id (dom ((S *') . f)) by Lm26 ; ::_thesis: verum
end;
let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies (S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g) )
assume A1: dom g = cod f ; ::_thesis: (S *') . (g (*) f) = ((S *') . f) (*) ((S *') . g)
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, Th16, A3
.= ((S *') . f) (*) ((S . g) opp) by Def11, A4, A5
.= ((S *') . f) (*) ((S *') . g) by Def11 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:59
for C, B, D being Category
for S1 being Contravariant_Functor of C,B
for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
proof
let C, B, D be Category; ::_thesis: for S1 being Contravariant_Functor of C,B
for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
let S1 be Contravariant_Functor of C,B; ::_thesis: for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
let S2 be Functor of B,D; ::_thesis: S2 * S1 is Contravariant_Functor of C,D
 *' S1 is Functor of C opp ,B by Th55;
then  S2 * (*' S1) is Functor of C opp ,D by CAT_1:73;
then  /* (S2 * (*' S1)) is Contravariant_Functor of C,D by Th34;
then  S2 * (/* (*' S1)) is Contravariant_Functor of C,D by Lm18;
hence  S2 * S1 is Contravariant_Functor of C,D by Th47; ::_thesis: verum
end;

theorem :: OPPCAT_1:60
for C, B, D being Category
for S1 being Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
proof
let C, B, D be Category; ::_thesis: for S1 being Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
let S1 be Functor of C,B; ::_thesis: for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
let S2 be Contravariant_Functor of B,D; ::_thesis: S2 * S1 is Contravariant_Functor of C,D
 *' S1 is Contravariant_Functor of C opp ,B by Th57;
then  S2 * (*' S1) is Functor of C opp ,D by Th35;
then  /* (S2 * (*' S1)) is Contravariant_Functor of C,D by Th34;
then  S2 * (/* (*' S1)) is Contravariant_Functor of C,D by Lm18;
hence  S2 * S1 is Contravariant_Functor of C,D by Th47; ::_thesis: verum
end;

theorem :: OPPCAT_1:61
for C, D being Category
for F being Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
proof
let C, D be Category; ::_thesis: for F being Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
let F be Functor of C,D; ::_thesis: for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
let c be Object of C; ::_thesis: (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
 *' F is Contravariant_Functor of C opp ,D by Th57;
hence (Obj ((*' F) *')) . (c opp) = ((Obj (*' F)) . (c opp)) opp by Th45
.= ((Obj F) . (opp (c opp))) opp by Th40
.= ((Obj F) . c) opp ;
::_thesis: verum
end;

theorem :: OPPCAT_1:62
for C, D being Category
for F being Contravariant_Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
proof
let C, D be Category; ::_thesis: for F being Contravariant_Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
let F be Contravariant_Functor of C,D; ::_thesis: for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
let c be Object of C; ::_thesis: (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
 *' F is Functor of C opp ,D by Th55;
hence (Obj ((*' F) *')) . (c opp) = ((Obj (*' F)) . (c opp)) opp by Th42
.= ((Obj F) . (opp (c opp))) opp by Th43
.= ((Obj F) . c) opp ;
::_thesis: verum
end;

theorem :: OPPCAT_1:63
for C, D being Category
for F being Functor of C,D holds (*' F) *' is Functor of C opp ,D opp
proof
let C, D be Category; ::_thesis: for F being Functor of C,D holds (*' F) *' is Functor of C opp ,D opp
let F be Functor of C,D; ::_thesis: (*' F) *' is Functor of C opp ,D opp
 *' F is Contravariant_Functor of C opp ,D by Th57;
hence  (*' F) *' is Functor of C opp ,D opp by Th56; ::_thesis: verum
end;

theorem :: OPPCAT_1:64
for C, D being Category
for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp
proof
let C, D be Category; ::_thesis: for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp
let F be Contravariant_Functor of C,D; ::_thesis: (*' F) *' is Contravariant_Functor of C opp ,D opp
 *' F is Functor of C opp ,D by Th55;
hence  (*' F) *' is Contravariant_Functor of C opp ,D opp by Th58; ::_thesis: verum
end;

definition
let C be Category;
func id* C ->  Contravariant_Functor of C,C opp  equals :: OPPCAT_1:def 12
(id C) *' ;
coherence
 (id C) *' is Contravariant_Functor of C,C opp by Th58;
func *id C ->  Contravariant_Functor of C opp ,C equals :: OPPCAT_1:def 13
 *' (id C);
coherence
 *' (id C) is Contravariant_Functor of C opp ,C by Th57;
end;

:: deftheorem  defines id* OPPCAT_1:def_12_:_
 for C being Category holds id* C = (id C) *' ;

:: deftheorem  defines *id OPPCAT_1:def_13_:_
 for C being Category holds *id C = *' (id C);

theorem Th65: :: OPPCAT_1:65
for C being Category
for f being Morphism of C holds (id* C) . f = f opp
proof
let C be Category; ::_thesis: for f being Morphism of C holds (id* C) . f = f opp
let f be Morphism of C; ::_thesis: (id* C) . f = f opp
thus (id* C) . f = ((id C) . f) opp by Def11
.= f opp by FUNCT_1:18 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:66
for C being Category
for c being Object of C holds (Obj (id* C)) . c = c opp
proof
let C be Category; ::_thesis: for c being Object of C holds (Obj (id* C)) . c = c opp
let c be Object of C; ::_thesis: (Obj (id* C)) . c = c opp
thus (Obj (id* C)) . c = ((Obj (id C)) . c) opp by Th42
.= c opp by CAT_1:77 ; ::_thesis: verum
end;

theorem Th67: :: OPPCAT_1:67
for C being Category
for f being Morphism of (C opp) holds (*id C) . f = opp f
proof
let C be Category; ::_thesis: for f being Morphism of (C opp) holds (*id C) . f = opp f
let f be Morphism of (C opp); ::_thesis: (*id C) . f = opp f
thus (*id C) . f = (id C) . (opp f) by Def10
.= opp f by FUNCT_1:18 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:68
for C being Category
for c being Object of (C opp) holds (Obj (*id C)) . c = opp c
proof
let C be Category; ::_thesis: for c being Object of (C opp) holds (Obj (*id C)) . c = opp c
let c be Object of (C opp); ::_thesis: (Obj (*id C)) . c = opp c
thus (Obj (*id C)) . c = (Obj (id C)) . (opp c) by Th40
.= opp c by CAT_1:77 ; ::_thesis: verum
end;

theorem :: OPPCAT_1:69
for C, D being Category
for S being Function of the carrier' of C, the carrier' of D holds
( *' S = S * (*id C) & S *' = (id* D) * S )
proof
let C, D be Category; ::_thesis: for S being Function of the carrier' of C, the carrier' of D holds
( *' S = S * (*id C) & S *' = (id* D) * S )
let S be Function of the carrier' of C, the carrier' of D; ::_thesis: ( *' S = S * (*id C) & S *' = (id* D) * S )
now__::_thesis:_for_f_being_Morphism_of_(C_opp)_holds_(*'_S)_._f_=_(S_*_(*id_C))_._f
let f be Morphism of (C opp); ::_thesis: (*' S) . f = (S * (*id C)) . f
thus (*' S) . f = S . (opp f) by Def10
.= S . ((*id C) . f) by Th67
.= (S * (*id C)) . f by FUNCT_2:15 ; ::_thesis: verum
end;
hence  *' S = S * (*id C) by FUNCT_2:63; ::_thesis: S *' = (id* D) * S
now__::_thesis:_for_f_being_Morphism_of_C_holds_(S_*')_._f_=_((id*_D)_*_S)_._f
let f be Morphism of C; ::_thesis: (S *') . f = ((id* D) * S) . f
thus (S *') . f = (S . f) opp by Def11
.= (id* D) . (S . f) by Th65
.= ((id* D) * S) . f by FUNCT_2:15 ; ::_thesis: verum
end;
hence  S *' = (id* D) * S by FUNCT_2:63; ::_thesis: verum
end;

theorem :: OPPCAT_1:70
for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (f opp) * (g opp) by Lm3;

theorem Th71: :: OPPCAT_1:71
for C being Category
for a being Object of C holds id a = id (a opp) by Lm2;

theorem :: OPPCAT_1:72
for C being Category
for a being Object of (C opp) holds id a = id (opp a)
proof
let C be Category; ::_thesis: for a being Object of (C opp) holds id a = id (opp a)
let a be Object of (C opp); ::_thesis: id a = id (opp a)
thus  id a = id ((opp a) opp)
.= id (opp a) by Th71 ; ::_thesis: verum
end;