:: OPPCAT_1 semantic presentation

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be PartFunc of [:c₁,c₂:],c₃;
redefine func ~ as ~ c₄ -> PartFunc of [:a₂,a₁:],a₃;
coherence by FUNCT_4:49;

end;

theorem Th1: :: OPPCAT_1:1

for b₁ being Category holds CatStr(# the Objects of b₁,the Morphisms of b₁,the Cod of b₁,the Dom of b₁,(~ the Comp of b₁),the Id of b₁ #) is Category

proof end;

definition

let c₁ be Category;
func c₁ opp -> strict Category equals :: OPPCAT_1:def 1
CatStr(# the Objects of a₁,the Morphisms of a₁,the Cod of a₁,the Dom of a₁,(~ the Comp of a₁),the Id of a₁ #);
coherence by Th1;

end;

:: deftheorem Def1 defines opp OPPCAT_1:def 1 :

theorem Th2: :: OPPCAT_1:2

for b₁ being Category holds (b₁ opp ) opp = CatStr(# the Objects of b₁,the Morphisms of b₁,the Dom of b₁,the Cod of b₁,the Comp of b₁,the Id of b₁ #) by FUNCT_4:54;

definition

let c₁ be Category;
let c₂ be Object of c₁;
func c₂ opp -> Object of (a₁ opp ) equals :: OPPCAT_1:def 2
a₂;
coherence ;

end;

:: deftheorem Def2 defines opp OPPCAT_1:def 2 :

definition

let c₁ be Category;
let c₂ be Object of (c₁ opp );
func opp c₂ -> Object of a₁ equals :: OPPCAT_1:def 3
a₂ opp ;
coherence ;

end;

:: deftheorem Def3 defines opp OPPCAT_1:def 3 :

theorem Th3: :: OPPCAT_1:3

for b₁ being Category
for b₂ being Object of b₁ holds (b₂ opp ) opp = b₂ ;

theorem Th4: :: OPPCAT_1:4

for b₁ being Category
for b₂ being Object of b₁ holds opp (b₂ opp ) = b₂ ;

theorem Th5: :: OPPCAT_1:5

for b₁ being Category
for b₂ being Object of (b₁ opp ) holds (opp b₂) opp = b₂ ;

definition

let c₁ be Category;
let c₂ be Morphism of c₁;
func c₂ opp -> Morphism of (a₁ opp ) equals :: OPPCAT_1:def 4
a₂;
coherence ;

end;

:: deftheorem Def4 defines opp OPPCAT_1:def 4 :

definition

let c₁ be Category;
let c₂ be Morphism of (c₁ opp );
func opp c₂ -> Morphism of a₁ equals :: OPPCAT_1:def 5
a₂ opp ;
coherence ;

end;

:: deftheorem Def5 defines opp OPPCAT_1:def 5 :

theorem Th6: :: OPPCAT_1:6

for b₁ being Category
for b₂ being Morphism of b₁ holds (b₂ opp ) opp = b₂ ;

theorem Th7: :: OPPCAT_1:7

for b₁ being Category
for b₂ being Morphism of b₁ holds opp (b₂ opp ) = b₂ ;

theorem Th8: :: OPPCAT_1:8

for b₁ being Category
for b₂ being Morphism of (b₁ opp ) holds (opp b₂) opp = b₂ ;

theorem Th9: :: OPPCAT_1:9

for b₁ being Category
for b₂ being Morphism of b₁ holds
( dom (b₂ opp ) = cod b₂ & cod (b₂ opp ) = dom b₂ ) ;

theorem Th10: :: OPPCAT_1:10

for b₁ being Category
for b₂ being Morphism of (b₁ opp ) holds
( dom (opp b₂) = cod b₂ & cod (opp b₂) = dom b₂ ) ;

theorem Th11: :: OPPCAT_1:11

for b₁ being Category
for b₂ being Morphism of b₁ holds
( (dom b₂) opp = cod (b₂ opp ) & (cod b₂) opp = dom (b₂ opp ) ) ;

theorem Th12: :: OPPCAT_1:12

for b₁ being Category
for b₂ being Morphism of (b₁ opp ) holds
( opp (dom b₂) = cod (opp b₂) & opp (cod b₂) = dom (opp b₂) ) ;

theorem Th13: :: OPPCAT_1:13

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₁ holds
( b₄ in Hom b₂,b₃ iff b₄ opp in Hom (b₃ opp ),(b₂ opp ) )

proof end;

theorem Th14: :: OPPCAT_1:14

for b₁ being Category
for b₂, b₃ being Object of (b₁ opp )
for b₄ being Morphism of (b₁ opp ) holds
( b₄ in Hom b₂,b₃ iff opp b₄ in Hom (opp b₃),(opp b₂) )

proof end;

theorem Th15: :: OPPCAT_1:15

for b₁ being Category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₂,b₃ st Hom b₂,b₃ <> {} holds
b₄ opp is Morphism of b₃ opp ,b₂ opp

proof end;

theorem Th16: :: OPPCAT_1:16

for b₁ being Category
for b₂, b₃ being Object of (b₁ opp )
for b₄ being Morphism of b₂,b₃ st Hom b₂,b₃ <> {} holds
opp b₄ is Morphism of opp b₃, opp b₂

proof end;

theorem Th17: :: OPPCAT_1:17

for b₁ being Category
for b₂, b₃ being Morphism of b₁ st dom b₃ = cod b₂ holds
(b₃ * b₂) opp = (b₂ opp ) * (b₃ opp )

proof end;

theorem Th18: :: OPPCAT_1:18

for b₁ being Category
for b₂, b₃ being Morphism of b₁ st cod (b₃ opp ) = dom (b₂ opp ) holds
(b₃ * b₂) opp = (b₂ opp ) * (b₃ opp )

proof end;

theorem Th19: :: OPPCAT_1:19

for b₁ being Category
for b₂, b₃ being Morphism of (b₁ opp ) st dom b₃ = cod b₂ holds
opp (b₃ * b₂) = (opp b₂) * (opp b₃)

proof end;

theorem Th20: :: OPPCAT_1:20

for b₁ being Category
for b₂, b₃, b₄ being Object of b₁
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₃,b₄ st Hom b₂,b₃ <> {} & Hom b₃,b₄ <> {} holds
(b₆ * b₅) opp = (b₅ opp ) * (b₆ opp )

proof end;

theorem Th21: :: OPPCAT_1:21

for b₁ being Category
for b₂ being Object of b₁ holds (id b₂) opp = id (b₂ opp ) ;

theorem Th22: :: OPPCAT_1:22

for b₁ being Category
for b₂ being Object of (b₁ opp ) holds opp (id b₂) = id (opp b₂) ;

theorem Th23: :: OPPCAT_1:23

for b₁ being Category
for b₂ being Morphism of b₁ holds
( b₂ opp is monic iff b₂ is epi )

proof end;

theorem Th24: :: OPPCAT_1:24

for b₁ being Category
for b₂ being Morphism of b₁ holds
( b₂ opp is epi iff b₂ is monic )

proof end;

theorem Th25: :: OPPCAT_1:25

for b₁ being Category
for b₂ being Morphism of b₁ holds
( b₂ opp is invertible iff b₂ is invertible )

proof end;

theorem Th26: :: OPPCAT_1:26

for b₁ being Category
for b₂ being Object of b₁ holds
( b₂ is initial iff b₂ opp is terminal )

proof end;

theorem Th27: :: OPPCAT_1:27

for b₁ being Category
for b₂ being Object of b₁ holds
( b₂ opp is initial iff b₂ is terminal )

proof end;

definition

let c₁, c₂ be Category;
let c₃ be Function of the Morphisms of (c₁ opp ),the Morphisms of c₂;
func /* c₃ -> Function of the Morphisms of a₁,the Morphisms of a₂ means :Def6: :: OPPCAT_1:def 6
for b₁ being Morphism of a₁ holds a₄ . b₁ = a₃ . (b₁ opp );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines /* OPPCAT_1:def 6 :

theorem Th28: :: OPPCAT_1:28

for b₁, b₂ being Category
for b₃ being Function of the Morphisms of (b₁ opp ),the Morphisms of b₂
for b₄ being Morphism of (b₁ opp ) holds (/* b₃) . (opp b₄) = b₃ . b₄

proof end;

Lemma11: for b₁, b₂ being Category
for b₃ being Functor of b₁ opp ,b₂
for b₄ being Object of b₁ holds (/* b₃) . (id b₄) = id ((Obj b₃) . (b₄ opp ))

proof end;

theorem Th29: :: OPPCAT_1:29

for b₁, b₂ being Category
for b₃ being Functor of b₁ opp ,b₂
for b₄ being Object of b₁ holds (Obj (/* b₃)) . b₄ = (Obj b₃) . (b₄ opp )

proof end;

theorem Th30: :: OPPCAT_1:30

for b₁, b₂ being Category
for b₃ being Functor of b₁ opp ,b₂
for b₄ being Object of (b₁ opp ) holds (Obj (/* b₃)) . (opp b₄) = (Obj b₃) . b₄

proof end;

Lemma13: for b₁, b₂ being Category
for b₃ being Functor of b₁ opp ,b₂
for b₄ being Object of b₁ holds (/* b₃) . (id b₄) = id ((Obj (/* b₃)) . b₄)

proof end;

E14: now

let c₁, c₂ be Category;
let c₃ be Functor of c₁ opp ,c₂;
let c₄ be Object of c₁;
(/* c₃) . (id c₄) = id ((Obj (/* c₃)) . c₄) by Lemma13;
hence ex b₁ being Object of c₂ st (/* c₃) . (id c₄) = id b₁ ;

end;

Lemma15: for b₁, b₂ being Category
for b₃ being Functor of b₁ opp ,b₂
for b₄ being Morphism of b₁ holds
( (Obj (/* b₃)) . (dom b₄) = cod ((/* b₃) . b₄) & (Obj (/* b₃)) . (cod b₄) = dom ((/* b₃) . b₄) )

proof end;

E16: now

let c₁, c₂ be Category;
let c₃ be Functor of c₁ opp ,c₂;
let c₄ be Morphism of c₁;
thus (/* c₃) . (id (dom c₄)) = id ((Obj (/* c₃)) . (dom c₄)) by Lemma13
.= id (cod ((/* c₃) . c₄)) by Lemma15 ;
thus (/* c₃) . (id (cod c₄)) = id ((Obj (/* c₃)) . (cod c₄)) by Lemma13
.= id (dom ((/* c₃) . c₄)) by Lemma15 ;

end;

Lemma17: for b₁, b₂ being Category
for b₃ being Functor of b₁ opp ,b₂
for b₄, b₅ being Morphism of b₁ st dom b₅ = cod b₄ holds
(/* b₃) . (b₅ * b₄) = ((/* b₃) . b₄) * ((/* b₃) . b₅)

proof end;

definition

let c₁, c₂ be Category;
mode Contravariant_Functor of c₁,c₂ -> Function of the Morphisms of a₁,the Morphisms of a₂ means :Def7: :: OPPCAT_1:def 7
( ( for b₁ being Object of a₁ ex b₂ being Object of a₂ st a₃ . (id b₁) = id b₂ ) & ( for b₁ being Morphism of a₁ holds
( a₃ . (id (dom b₁)) = id (cod (a₃ . b₁)) & a₃ . (id (cod b₁)) = id (dom (a₃ . b₁)) ) ) & ( for b₁, b₂ being Morphism of a₁ st dom b₂ = cod b₁ holds
a₃ . (b₂ * b₁) = (a₃ . b₁) * (a₃ . b₂) ) );
existence

proof end;

end;

:: deftheorem Def7 defines Contravariant_Functor OPPCAT_1:def 7 :

theorem Th31: :: OPPCAT_1:31

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of b₁
for b₅ being Object of b₂ st b₃ . (id b₄) = id b₅ holds
(Obj b₃) . b₄ = b₅

proof end;

theorem Th32: :: OPPCAT_1:32

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of b₁ holds b₃ . (id b₄) = id ((Obj b₃) . b₄)

proof end;

theorem Th33: :: OPPCAT_1:33

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Morphism of b₁ holds
( (Obj b₃) . (dom b₄) = cod (b₃ . b₄) & (Obj b₃) . (cod b₄) = dom (b₃ . b₄) )

proof end;

theorem Th34: :: OPPCAT_1:34

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄, b₅ being Morphism of b₁ st dom b₅ = cod b₄ holds
dom (b₃ . b₄) = cod (b₃ . b₅)

proof end;

theorem Th35: :: OPPCAT_1:35

for b₁, b₂ being Category
for b₃ being Functor of b₁ opp ,b₂ holds /* b₃ is Contravariant_Functor of b₁,b₂

proof end;

theorem Th36: :: OPPCAT_1:36

for b₁, b₂, b₃ being Category
for b₄ being Contravariant_Functor of b₁,b₂
for b₅ being Contravariant_Functor of b₂,b₃ holds b₅ * b₄ is Functor of b₁,b₃

proof end;

Lemma25: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁ opp ,b₂
for b₄ being Object of b₁ holds (/* b₃) . (id b₄) = id ((Obj b₃) . (b₄ opp ))

proof end;

theorem Th37: :: OPPCAT_1:37

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁ opp ,b₂
for b₄ being Object of b₁ holds (Obj (/* b₃)) . b₄ = (Obj b₃) . (b₄ opp )

proof end;

theorem Th38: :: OPPCAT_1:38

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁ opp ,b₂
for b₄ being Object of (b₁ opp ) holds (Obj (/* b₃)) . (opp b₄) = (Obj b₃) . b₄

proof end;

Lemma27: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁ opp ,b₂
for b₄ being Object of b₁ holds (/* b₃) . (id b₄) = id ((Obj (/* b₃)) . b₄)

proof end;

Lemma28: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁ opp ,b₂
for b₄ being Morphism of b₁ holds
( (Obj (/* b₃)) . (dom b₄) = dom ((/* b₃) . b₄) & (Obj (/* b₃)) . (cod b₄) = cod ((/* b₃) . b₄) )

proof end;

theorem Th39: :: OPPCAT_1:39

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁ opp ,b₂ holds /* b₃ is Functor of b₁,b₂

proof end;

definition

let c₁, c₂ be Category;
let c₃ be Function of the Morphisms of c₁,the Morphisms of c₂;
func *' c₃ -> Function of the Morphisms of (a₁ opp ),the Morphisms of a₂ means :Def8: :: OPPCAT_1:def 8
for b₁ being Morphism of (a₁ opp ) holds a₄ . b₁ = a₃ . (opp b₁);
existence

proof end;

uniqueness

proof end;

func c₃ *' -> Function of the Morphisms of a₁,the Morphisms of (a₂ opp ) means :Def9: :: OPPCAT_1:def 9
for b₁ being Morphism of a₁ holds a₄ . b₁ = (a₃ . b₁) opp ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines *' OPPCAT_1:def 8 :

:: deftheorem Def9 defines *' OPPCAT_1:def 9 :

theorem Th40: :: OPPCAT_1:40

for b₁, b₂ being Category
for b₃ being Function of the Morphisms of b₁,the Morphisms of b₂
for b₄ being Morphism of b₁ holds (*' b₃) . (b₄ opp ) = b₃ . b₄

proof end;

Lemma31: for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of (b₁ opp ) holds (*' b₃) . (id b₄) = id ((Obj b₃) . (opp b₄))

proof end;

theorem Th41: :: OPPCAT_1:41

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of (b₁ opp ) holds (Obj (*' b₃)) . b₄ = (Obj b₃) . (opp b₄)

proof end;

theorem Th42: :: OPPCAT_1:42

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of b₁ holds (Obj (*' b₃)) . (b₄ opp ) = (Obj b₃) . b₄

proof end;

Lemma33: for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of b₁ holds (b₃ *' ) . (id b₄) = id (((Obj b₃) . b₄) opp )

proof end;

theorem Th43: :: OPPCAT_1:43

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of b₁ holds (Obj (b₃ *' )) . b₄ = ((Obj b₃) . b₄) opp

proof end;

Lemma35: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of (b₁ opp ) holds (*' b₃) . (id b₄) = id ((Obj b₃) . (opp b₄))

proof end;

theorem Th44: :: OPPCAT_1:44

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of (b₁ opp ) holds (Obj (*' b₃)) . b₄ = (Obj b₃) . (opp b₄)

proof end;

theorem Th45: :: OPPCAT_1:45

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of b₁ holds (Obj (*' b₃)) . (b₄ opp ) = (Obj b₃) . b₄

proof end;

Lemma37: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of b₁ holds (b₃ *' ) . (id b₄) = id (((Obj b₃) . b₄) opp )

proof end;

theorem Th46: :: OPPCAT_1:46

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of b₁ holds (Obj (b₃ *' )) . b₄ = ((Obj b₃) . b₄) opp

proof end;

Lemma39: for b₁, b₂ being Category
for b₃ being Function of the Morphisms of b₁,the Morphisms of b₂
for b₄ being Morphism of (b₁ opp ) holds ((*' b₃) *' ) . b₄ = (b₃ . (opp b₄)) opp

proof end;

theorem Th47: :: OPPCAT_1:47

for b₁, b₂ being Category
for b₃ being Function of the Morphisms of b₁,the Morphisms of b₂
for b₄ being Morphism of b₁ holds ((*' b₃) *' ) . (b₄ opp ) = (b₃ . b₄) opp

proof end;

theorem Th48: :: OPPCAT_1:48

for b₁, b₂ being Category
for b₃ being Function of the Morphisms of b₁,the Morphisms of b₂ holds /* (*' b₃) = b₃

proof end;

theorem Th49: :: OPPCAT_1:49

for b₁, b₂ being Category
for b₃ being Function of the Morphisms of (b₁ opp ),the Morphisms of b₂ holds *' (/* b₃) = b₃

proof end;

theorem Th50: :: OPPCAT_1:50

for b₁, b₂ being Category
for b₃ being Function of the Morphisms of b₁,the Morphisms of b₂ holds (*' b₃) *' = *' (b₃ *' )

proof end;

theorem Th51: :: OPPCAT_1:51

for b₁ being Category
for b₂ being strict Category
for b₃ being Function of the Morphisms of b₁,the Morphisms of b₂ holds (b₃ *' ) *' = b₃

proof end;

theorem Th52: :: OPPCAT_1:52

for b₁ being Category
for b₂ being strict Category
for b₃ being Function of the Morphisms of b₂,the Morphisms of b₁ holds *' (*' b₃) = b₃

proof end;

Lemma42: for b₁, b₂, b₃ being Category
for b₄ being Function of the Morphisms of (b₁ opp ),the Morphisms of b₂
for b₅ being Function of the Morphisms of b₂,the Morphisms of b₃ holds /* (b₅ * b₄) = b₅ * (/* b₄)

proof end;

theorem Th53: :: OPPCAT_1:53

for b₁, b₂, b₃ being Category
for b₄ being Function of the Morphisms of b₁,the Morphisms of b₂
for b₅ being Function of the Morphisms of b₂,the Morphisms of b₃ holds *' (b₅ * b₄) = b₅ * (*' b₄)

proof end;

theorem Th54: :: OPPCAT_1:54

for b₁, b₂, b₃ being Category
for b₄ being Function of the Morphisms of b₁,the Morphisms of b₂
for b₅ being Function of the Morphisms of b₂,the Morphisms of b₃ holds (b₅ * b₄) *' = (b₅ *' ) * b₄

proof end;

theorem Th55: :: OPPCAT_1:55

for b₁, b₂, b₃ being Category
for b₄ being Function of the Morphisms of b₁,the Morphisms of b₂
for b₅ being Function of the Morphisms of b₂,the Morphisms of b₃ holds (*' (b₅ * b₄)) *' = ((*' b₅) *' ) * ((*' b₄) *' )

proof end;

Lemma43: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of (b₁ opp ) holds (*' b₃) . (id b₄) = id ((Obj (*' b₃)) . b₄)

proof end;

Lemma44: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Morphism of (b₁ opp ) holds
( (Obj (*' b₃)) . (dom b₄) = dom ((*' b₃) . b₄) & (Obj (*' b₃)) . (cod b₄) = cod ((*' b₃) . b₄) )

proof end;

theorem Th56: :: OPPCAT_1:56

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂ holds *' b₃ is Functor of b₁ opp ,b₂

proof end;

Lemma46: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of b₁ holds (b₃ *' ) . (id b₄) = id ((Obj (b₃ *' )) . b₄)

proof end;

Lemma47: for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Morphism of b₁ holds
( (Obj (b₃ *' )) . (dom b₄) = dom ((b₃ *' ) . b₄) & (Obj (b₃ *' )) . (cod b₄) = cod ((b₃ *' ) . b₄) )

proof end;

theorem Th57: :: OPPCAT_1:57

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂ holds b₃ *' is Functor of b₁,b₂ opp

proof end;

Lemma49: for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of (b₁ opp ) holds (*' b₃) . (id b₄) = id ((Obj (*' b₃)) . b₄)

proof end;

Lemma50: for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Morphism of (b₁ opp ) holds
( (Obj (*' b₃)) . (dom b₄) = cod ((*' b₃) . b₄) & (Obj (*' b₃)) . (cod b₄) = dom ((*' b₃) . b₄) )

proof end;

theorem Th58: :: OPPCAT_1:58

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ holds *' b₃ is Contravariant_Functor of b₁ opp ,b₂

proof end;

Lemma52: for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of b₁ holds (b₃ *' ) . (id b₄) = id ((Obj (b₃ *' )) . b₄)

proof end;

Lemma53: for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Morphism of b₁ holds
( (Obj (b₃ *' )) . (dom b₄) = cod ((b₃ *' ) . b₄) & (Obj (b₃ *' )) . (cod b₄) = dom ((b₃ *' ) . b₄) )

proof end;

theorem Th59: :: OPPCAT_1:59

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ holds b₃ *' is Contravariant_Functor of b₁,b₂ opp

proof end;

theorem Th60: :: OPPCAT_1:60

for b₁, b₂, b₃ being Category
for b₄ being Contravariant_Functor of b₁,b₂
for b₅ being Functor of b₂,b₃ holds b₅ * b₄ is Contravariant_Functor of b₁,b₃

proof end;

theorem Th61: :: OPPCAT_1:61

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Contravariant_Functor of b₂,b₃ holds b₅ * b₄ is Contravariant_Functor of b₁,b₃

proof end;

theorem Th62: :: OPPCAT_1:62

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of b₁ holds (Obj ((*' b₃) *' )) . (b₄ opp ) = ((Obj b₃) . b₄) opp

proof end;

theorem Th63: :: OPPCAT_1:63

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂
for b₄ being Object of b₁ holds (Obj ((*' b₃) *' )) . (b₄ opp ) = ((Obj b₃) . b₄) opp

proof end;

theorem Th64: :: OPPCAT_1:64

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ holds (*' b₃) *' is Functor of b₁ opp ,b₂ opp

proof end;

theorem Th65: :: OPPCAT_1:65

for b₁, b₂ being Category
for b₃ being Contravariant_Functor of b₁,b₂ holds (*' b₃) *' is Contravariant_Functor of b₁ opp ,b₂ opp

proof end;

definition

let c₁ be Category;
func id* c₁ -> Contravariant_Functor of a₁,a₁ opp equals :: OPPCAT_1:def 10
(id a₁) *' ;
coherence by Th59;
func *id c₁ -> Contravariant_Functor of a₁ opp ,a₁ equals :: OPPCAT_1:def 11
*' (id a₁);
coherence by Th58;

end;

:: deftheorem Def10 defines id* OPPCAT_1:def 10 :

:: deftheorem Def11 defines *id OPPCAT_1:def 11 :

theorem Th66: :: OPPCAT_1:66

for b₁ being Category
for b₂ being Morphism of b₁ holds (id* b₁) . b₂ = b₂ opp

proof end;

theorem Th67: :: OPPCAT_1:67

for b₁ being Category
for b₂ being Object of b₁ holds (Obj (id* b₁)) . b₂ = b₂ opp

proof end;

theorem Th68: :: OPPCAT_1:68

for b₁ being Category
for b₂ being Morphism of (b₁ opp ) holds (*id b₁) . b₂ = opp b₂

proof end;

theorem Th69: :: OPPCAT_1:69

for b₁ being Category
for b₂ being Object of (b₁ opp ) holds (Obj (*id b₁)) . b₂ = opp b₂

proof end;

theorem Th70: :: OPPCAT_1:70

for b₁, b₂ being Category
for b₃ being Function of the Morphisms of b₁,the Morphisms of b₂ holds
( *' b₃ = b₃ * (*id b₁) & b₃ *' = (id* b₂) * b₃ )

proof end;