:: YELLOW20 semantic presentation

theorem Th1: :: YELLOW20:1

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being reflexive feasible FunctorStr of b₁,b₂ st b₃ is coreflexive & b₃ is bijective holds
for b₄ being object of b₁
for b₅ being object of b₂ holds
( b₃ . b₄ = b₅ iff (b₃ " ) . b₅ = b₄ )

proof end;

theorem Th2: :: YELLOW20:2

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being feasible Covariant FunctorStr of b₁,b₂
for b₄ being feasible Covariant FunctorStr of b₂,b₁ st b₃ is bijective & b₄ = b₃ " holds
for b₅, b₆ being object of b₁ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆
for b₈ being Morphism of (b₃ . b₅),(b₃ . b₆) holds
( b₃ . b₇ = b₈ iff b₄ . b₈ = b₇ )

proof end;

theorem Th3: :: YELLOW20:3

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being feasible Contravariant FunctorStr of b₁,b₂
for b₄ being feasible Contravariant FunctorStr of b₂,b₁ st b₃ is bijective & b₄ = b₃ " holds
for b₅, b₆ being object of b₁ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆
for b₈ being Morphism of (b₃ . b₆),(b₃ . b₅) holds
( b₃ . b₇ = b₈ iff b₄ . b₈ = b₇ )

proof end;

theorem Th4: :: YELLOW20:4

for b₁, b₂ being category
for b₃ being Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being Functor of b₂,b₁ st b₃ * b₄ = id b₂ holds
FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = b₃ "

proof end;

theorem Th5: :: YELLOW20:5

for b₁, b₂ being category
for b₃ being Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being Functor of b₂,b₁ st b₄ * b₃ = id b₁ holds
FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = b₃ "

proof end;

theorem Th6: :: YELLOW20:6

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being covariant Functor of b₂,b₁ st ( for b₅ being object of b₂ holds b₃ . (b₄ . b₅) = b₅ ) & ( for b₅, b₆ being object of b₂ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₃ . (b₄ . b₇) = b₇ ) holds
FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = b₃ "

proof end;

theorem Th7: :: YELLOW20:7

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being contravariant Functor of b₂,b₁ st ( for b₅ being object of b₂ holds b₃ . (b₄ . b₅) = b₅ ) & ( for b₅, b₆ being object of b₂ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₃ . (b₄ . b₇) = b₇ ) holds
FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = b₃ "

proof end;

theorem Th8: :: YELLOW20:8

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being covariant Functor of b₂,b₁ st ( for b₅ being object of b₁ holds b₄ . (b₃ . b₅) = b₅ ) & ( for b₅, b₆ being object of b₁ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₄ . (b₃ . b₇) = b₇ ) holds
FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = b₃ "

proof end;

theorem Th9: :: YELLOW20:9

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being contravariant Functor of b₂,b₁ st ( for b₅ being object of b₁ holds b₄ . (b₃ . b₅) = b₅ ) & ( for b₅, b₆ being object of b₁ st <^b₅,b₆^> <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₄ . (b₃ . b₇) = b₇ ) holds
FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = b₃ "

proof end;

definition

let c₁, c₂ be AltCatStr ;
pred c₁,c₂ have_the_same_composition means :Def1: :: YELLOW20:def 1
for b₁, b₂, b₃ being set holds the Comp of a₁ . [b₁,b₂,b₃] tolerates the Comp of a₂ . [b₁,b₂,b₃];
symmetry ;

end;

:: deftheorem Def1 defines have_the_same_composition YELLOW20:def 1 :

theorem Th10: :: YELLOW20:10

for b₁, b₂ being AltCatStr holds
( b₁,b₂ have_the_same_composition iff for b₃, b₄, b₅, b₆ being set st b₆ in dom (the Comp of b₁ . [b₃,b₄,b₅]) & b₆ in dom (the Comp of b₂ . [b₃,b₄,b₅]) holds
(the Comp of b₁ . [b₃,b₄,b₅]) . b₆ = (the Comp of b₂ . [b₃,b₄,b₅]) . b₆ )

proof end;

theorem Th11: :: YELLOW20:11

for b₁, b₂ being non empty transitive AltCatStr holds
( b₁,b₂ have_the_same_composition iff for b₃, b₄, b₅ being object of b₁ st <^b₃,b₄^> <> {} & <^b₄,b₅^> <> {} holds
for b₆, b₇, b₈ being object of b₂ st <^b₆,b₇^> <> {} & <^b₇,b₈^> <> {} & b₆ = b₃ & b₇ = b₄ & b₈ = b₅ holds
for b₉ being Morphism of b₃,b₄
for b₁₀ being Morphism of b₆,b₇ st b₁₀ = b₉ holds
for b₁₁ being Morphism of b₄,b₅
for b₁₂ being Morphism of b₇,b₈ st b₁₂ = b₁₁ holds
b₁₁ * b₉ = b₁₂ * b₁₀ )

proof end;

theorem Th12: :: YELLOW20:12

for b₁, b₂ being semi-functional para-functional category holds b₁,b₂ have_the_same_composition

proof end;

definition

let c₁, c₂ be Function;
func Intersect c₁,c₂ -> Function means :Def2: :: YELLOW20:def 2
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in (dom a₁) /\ (dom a₂) holds
a₃ . b₁ = (a₁ . b₁) /\ (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def2 defines Intersect YELLOW20:def 2 :

theorem Th13: :: YELLOW20:13

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ holds Intersect b₂,b₃ = b₂ /\ b₃

proof end;

theorem Th14: :: YELLOW20:14

for b₁, b₂ being set
for b₃ being ManySortedSet of b₁
for b₄ being ManySortedSet of b₂ holds Intersect b₃,b₄ is ManySortedSet of b₁ /\ b₂

proof end;

theorem Th15: :: YELLOW20:15

for b₁, b₂ being set
for b₃ being ManySortedSet of b₁
for b₄ being Function
for b₅ being ManySortedSet of b₂ st b₅ = Intersect b₃,b₄ holds
b₅ cc= b₃

proof end;

theorem Th16: :: YELLOW20:16

for b₁, b₂, b₃, b₄ being set
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ st b₅ tolerates b₆ holds
b₅ /\ b₆ is Function of b₁ /\ b₃,b₂ /\ b₄

proof end;

theorem Th17: :: YELLOW20:17

for b₁, b₂ being set
for b₃, b₄ being ManySortedSet of b₁
for b₅, b₆ being ManySortedSet of b₂
for b₇, b₈ being ManySortedSet of b₁ /\ b₂ st b₇ = Intersect b₃,b₅ & b₈ = Intersect b₄,b₆ holds
for b₉ being ManySortedFunction of b₃,b₄
for b₁₀ being ManySortedFunction of b₅,b₆ st ( for b₁₁ being set st b₁₁ in dom b₉ & b₁₁ in dom b₁₀ holds
b₉ . b₁₁ tolerates b₁₀ . b₁₁ ) holds
Intersect b₉,b₁₀ is ManySortedFunction of b₇,b₈

proof end;

theorem Th18: :: YELLOW20:18

for b₁, b₂ being set
for b₃ being ManySortedSet of [:b₁,b₁:]
for b₄ being ManySortedSet of [:b₂,b₂:] ex b₅ being ManySortedSet of [:(b₁ /\ b₂),(b₁ /\ b₂):] st
( b₅ = Intersect b₃,b₄ & Intersect {|b₃|},{|b₄|} = {|b₅|} )

proof end;

theorem Th19: :: YELLOW20:19

for b₁, b₂ being set
for b₃, b₄ being ManySortedSet of [:b₁,b₁:]
for b₅, b₆ being ManySortedSet of [:b₂,b₂:] ex b₇, b₈ being ManySortedSet of [:(b₁ /\ b₂),(b₁ /\ b₂):] st
( b₇ = Intersect b₃,b₅ & b₈ = Intersect b₄,b₆ & Intersect {|b₃,b₄|},{|b₅,b₆|} = {|b₇,b₈|} )

proof end;

definition

let c₁, c₂ be AltCatStr ;
assume E16: c₁,c₂ have_the_same_composition ;
func Intersect c₁,c₂ -> strict AltCatStr means :Def3: :: YELLOW20:def 3
( the carrier of a₃ = the carrier of a₁ /\ the carrier of a₂ & the Arrows of a₃ = Intersect the Arrows of a₁,the Arrows of a₂ & the Comp of a₃ = Intersect the Comp of a₁,the Comp of a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def3 defines Intersect YELLOW20:def 3 :

theorem Th20: :: YELLOW20:20

for b₁, b₂ being AltCatStr st b₁,b₂ have_the_same_composition holds
Intersect b₁,b₂ = Intersect b₂,b₁

proof end;

theorem Th21: :: YELLOW20:21

for b₁, b₂ being AltCatStr st b₁,b₂ have_the_same_composition holds
Intersect b₁,b₂ is SubCatStr of b₁

proof end;

theorem Th22: :: YELLOW20:22

for b₁, b₂ being AltCatStr st b₁,b₂ have_the_same_composition holds
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂
for b₇, b₈ being object of (Intersect b₁,b₂) st b₇ = b₃ & b₇ = b₅ & b₈ = b₄ & b₈ = b₆ holds
<^b₇,b₈^> = <^b₃,b₄^> /\ <^b₅,b₆^>

proof end;

theorem Th23: :: YELLOW20:23

for b₁, b₂ being transitive AltCatStr st b₁,b₂ have_the_same_composition holds
Intersect b₁,b₂ is transitive

proof end;

theorem Th24: :: YELLOW20:24

for b₁, b₂ being AltCatStr st b₁,b₂ have_the_same_composition holds
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂
for b₇, b₈ being object of (Intersect b₁,b₂) st b₇ = b₃ & b₇ = b₅ & b₈ = b₄ & b₈ = b₆ & <^b₃,b₄^> <> {} & <^b₅,b₆^> <> {} holds
for b₉ being Morphism of b₃,b₄
for b₁₀ being Morphism of b₅,b₆ st b₉ = b₁₀ holds
b₉ in <^b₇,b₈^>

proof end;

theorem Th25: :: YELLOW20:25

for b₁, b₂ being non empty with_units AltCatStr st b₁,b₂ have_the_same_composition holds
for b₃ being object of b₁
for b₄ being object of b₂
for b₅ being object of (Intersect b₁,b₂) st b₅ = b₃ & b₅ = b₄ & idm b₃ = idm b₄ holds
idm b₃ in <^b₅,b₅^> by Th24;

theorem Th26: :: YELLOW20:26

for b₁, b₂ being category st b₁,b₂ have_the_same_composition & not Intersect b₁,b₂ is empty & ( for b₃ being object of b₁
for b₄ being object of b₂ st b₃ = b₄ holds
idm b₃ = idm b₄ ) holds
Intersect b₁,b₂ is subcategory of b₁

proof end;

scheme :: YELLOW20:sch 1
s1{ F₁() -> category, F₂() -> non empty subcategory of F₁(), F₃() -> non empty subcategory of F₁(), P₁[ set ], P₂[ set , set , set ] } :

AltCatStr(# the carrier of F₂(),the Arrows of F₂(),the Comp of F₂() #) = AltCatStr(# the carrier of F₃(),the Arrows of F₃(),the Comp of F₃() #)

provided

E21: for b₁ being object of F₁() holds
( b₁ is object of F₂() iff P₁[b₁] ) and
E22: for b₁, b₂ being object of F₁()
for b₃, b₄ being object of F₂() st b₃ = b₁ & b₄ = b₂ & <^b₁,b₂^> <> {} holds
for b₅ being Morphism of b₁,b₂ holds
( b₅ in <^b₃,b₄^> iff P₂[b₁,b₂,b₅] ) and
E23: for b₁ being object of F₁() holds
( b₁ is object of F₃() iff P₁[b₁] ) and
E24: for b₁, b₂ being object of F₁()
for b₃, b₄ being object of F₃() st b₃ = b₁ & b₄ = b₂ & <^b₁,b₂^> <> {} holds
for b₅ being Morphism of b₁,b₂ holds
( b₅ in <^b₃,b₄^> iff P₂[b₁,b₂,b₅] )

proof end;

theorem Th27: :: YELLOW20:27

for b₁ being non empty AltCatStr
for b₂ being non empty SubCatStr of b₁ holds
( b₂ is full iff for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂ st b₅ = b₃ & b₆ = b₄ holds
<^b₅,b₆^> = <^b₃,b₄^> )

proof end;

scheme :: YELLOW20:sch 2
s2{ F₁() -> category, P₁[ set ] } :

ex b₁ being non empty strict full subcategory of F₁() st
for b₂ being object of F₁() holds
( b₂ is object of b₁ iff P₁[b₂] )

provided

E22: ex b₁ being object of F₁() st P₁[b₁]

proof end;

scheme :: YELLOW20:sch 3
s3{ F₁() -> category, F₂() -> non empty full subcategory of F₁(), F₃() -> non empty full subcategory of F₁(), P₁[ set ] } :

AltCatStr(# the carrier of F₂(),the Arrows of F₂(),the Comp of F₂() #) = AltCatStr(# the carrier of F₃(),the Arrows of F₃(),the Comp of F₃() #)

provided

E22: for b₁ being object of F₁() holds
( b₁ is object of F₂() iff P₁[b₁] ) and
E23: for b₁ being object of F₁() holds
( b₁ is object of F₃() iff P₁[b₁] )

proof end;

registration

let c₁ be Function-yielding Function;
let c₂, c₃ be set ;
cluster a₁ . a₂,a₃ -> Relation-like Function-like ;
coherence

proof end;

end;

theorem Th28: :: YELLOW20:28

for b₁ being category
for b₂ being non empty subcategory of b₁
for b₃, b₄ being object of b₂ st <^b₃,b₄^> <> {} holds
for b₅ being Morphism of b₃,b₄ holds (incl b₂) . b₅ = b₅

proof end;

registration

let c₁ be category;
let c₂ be non empty subcategory of c₁;
cluster incl a₂ -> id-preserving comp-preserving ;
coherence

proof end;

end;

registration

let c₁ be category;
let c₂ be non empty subcategory of c₁;
cluster incl a₂ -> Covariant id-preserving comp-preserving ;
coherence ;

end;

definition

let c₁ be category;
let c₂ be non empty subcategory of c₁;
redefine func incl as incl c₂ -> strict covariant Functor of a₂,a₁;
coherence by FUNCTOR0:def 26, FUNCTOR0:def 27;

end;

definition

let c₁, c₂ be category;
let c₃ be non empty subcategory of c₁;
let c₄ be covariant Functor of c₁,c₂;
redefine func | as c₄ | c₃ -> strict covariant Functor of a₃,a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be category;
let c₃ be non empty subcategory of c₁;
let c₄ be contravariant Functor of c₁,c₂;
redefine func | as c₄ | c₃ -> strict contravariant Functor of a₃,a₂;
coherence

proof end;

end;

theorem Th29: :: YELLOW20:29

for b₁, b₂ being category
for b₃ being non empty subcategory of b₁
for b₄ being FunctorStr of b₁,b₂
for b₅ being object of b₁
for b₆ being object of b₃ st b₆ = b₅ holds
(b₄ | b₃) . b₆ = b₄ . b₅

proof end;

theorem Th30: :: YELLOW20:30

for b₁, b₂ being category
for b₃ being non empty subcategory of b₁
for b₄ being covariant Functor of b₁,b₂
for b₅, b₆ being object of b₁
for b₇, b₈ being object of b₃ st b₇ = b₅ & b₈ = b₆ & <^b₇,b₈^> <> {} holds
for b₉ being Morphism of b₅,b₆
for b₁₀ being Morphism of b₇,b₈ st b₁₀ = b₉ holds
(b₄ | b₃) . b₁₀ = b₄ . b₉

proof end;

theorem Th31: :: YELLOW20:31

for b₁, b₂ being category
for b₃ being non empty subcategory of b₁
for b₄ being contravariant Functor of b₁,b₂
for b₅, b₆ being object of b₁
for b₇, b₈ being object of b₃ st b₇ = b₅ & b₈ = b₆ & <^b₇,b₈^> <> {} holds
for b₉ being Morphism of b₅,b₆
for b₁₀ being Morphism of b₇,b₈ st b₁₀ = b₉ holds
(b₄ | b₃) . b₁₀ = b₄ . b₉

proof end;

theorem Th32: :: YELLOW20:32

for b₁, b₂ being non empty AltGraph
for b₃ being BimapStr of b₁,b₂ st b₃ is Covariant & b₃ is one-to-one holds
for b₄, b₅ being object of b₁ st b₃ . b₄ = b₃ . b₅ holds
b₄ = b₅

proof end;

theorem Th33: :: YELLOW20:33

for b₁, b₂ being non empty reflexive AltGraph
for b₃ being feasible Covariant FunctorStr of b₁,b₂ st b₃ is faithful holds
for b₄, b₅ being object of b₁ st <^b₄,b₅^> <> {} holds
for b₆, b₇ being Morphism of b₄,b₅ st b₃ . b₆ = b₃ . b₇ holds
b₆ = b₇

proof end;

theorem Th34: :: YELLOW20:34

for b₁, b₂ being non empty AltGraph
for b₃ being Covariant FunctorStr of b₁,b₂ st b₃ is surjective holds
for b₄, b₅ being object of b₂ st <^b₄,b₅^> <> {} holds
for b₆ being Morphism of b₄,b₅ ex b₇, b₈ being object of b₁ex b₉ being Morphism of b₇,b₈ st
( b₄ = b₃ . b₇ & b₅ = b₃ . b₈ & <^b₇,b₈^> <> {} & b₆ = b₃ . b₉ )

proof end;

theorem Th35: :: YELLOW20:35

for b₁, b₂ being non empty AltGraph
for b₃ being BimapStr of b₁,b₂ st b₃ is Contravariant & b₃ is one-to-one holds
for b₄, b₅ being object of b₁ st b₃ . b₄ = b₃ . b₅ holds
b₄ = b₅

proof end;

theorem Th36: :: YELLOW20:36

for b₁, b₂ being non empty reflexive AltGraph
for b₃ being feasible Contravariant FunctorStr of b₁,b₂ st b₃ is faithful holds
for b₄, b₅ being object of b₁ st <^b₄,b₅^> <> {} holds
for b₆, b₇ being Morphism of b₄,b₅ st b₃ . b₆ = b₃ . b₇ holds
b₆ = b₇

proof end;

theorem Th37: :: YELLOW20:37

for b₁, b₂ being non empty AltGraph
for b₃ being Contravariant FunctorStr of b₁,b₂ st b₃ is surjective holds
for b₄, b₅ being object of b₂ st <^b₄,b₅^> <> {} holds
for b₆ being Morphism of b₄,b₅ ex b₇, b₈ being object of b₁ex b₉ being Morphism of b₇,b₈ st
( b₅ = b₃ . b₇ & b₄ = b₃ . b₈ & <^b₇,b₈^> <> {} & b₆ = b₃ . b₉ )

proof end;

definition

let c₁, c₂ be category;
let c₃ be FunctorStr of c₁,c₂;
let c₄, c₅ be category;
pred c₄,c₅ are_isomorphic_under c₃ means :: YELLOW20:def 4
( a₄ is subcategory of a₁ & a₅ is subcategory of a₂ & ex b₁ being covariant Functor of a₄,a₅ st
( b₁ is bijective & ( for b₂ being object of a₄
for b₃ being object of a₁ st b₂ = b₃ holds
b₁ . b₂ = a₃ . b₃ ) & ( for b₂, b₃ being object of a₄
for b₄, b₅ being object of a₁ st <^b₂,b₃^> <> {} & b₂ = b₄ & b₃ = b₅ holds
for b₆ being Morphism of b₂,b₃
for b₇ being Morphism of b₄,b₅ st b₆ = b₇ holds
b₁ . b₆ = (Morph-Map a₃,b₄,b₅) . b₇ ) ) );
pred c₄,c₅ are_anti-isomorphic_under c₃ means :: YELLOW20:def 5
( a₄ is subcategory of a₁ & a₅ is subcategory of a₂ & ex b₁ being contravariant Functor of a₄,a₅ st
( b₁ is bijective & ( for b₂ being object of a₄
for b₃ being object of a₁ st b₂ = b₃ holds
b₁ . b₂ = a₃ . b₃ ) & ( for b₂, b₃ being object of a₄
for b₄, b₅ being object of a₁ st <^b₂,b₃^> <> {} & b₂ = b₄ & b₃ = b₅ holds
for b₆ being Morphism of b₂,b₃
for b₇ being Morphism of b₄,b₅ st b₆ = b₇ holds
b₁ . b₆ = (Morph-Map a₃,b₄,b₅) . b₇ ) ) );

end;

:: deftheorem Def4 defines are_isomorphic_under YELLOW20:def 4 :

:: deftheorem Def5 defines are_anti-isomorphic_under YELLOW20:def 5 :

theorem Th38: :: YELLOW20:38

for b₁, b₂, b₃, b₄ being category
for b₅ being FunctorStr of b₁,b₂ st b₃,b₄ are_isomorphic_under b₅ holds
b₃,b₄ are_isomorphic

proof end;

theorem Th39: :: YELLOW20:39

for b₁, b₂, b₃, b₄ being category
for b₅ being FunctorStr of b₁,b₂ st b₃,b₄ are_anti-isomorphic_under b₅ holds
b₃,b₄ are_anti-isomorphic

proof end;

theorem Th40: :: YELLOW20:40

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂ st b₁,b₂ are_isomorphic_under b₃ holds
b₃ is bijective

proof end;

theorem Th41: :: YELLOW20:41

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂ st b₁,b₂ are_anti-isomorphic_under b₃ holds
b₃ is bijective

proof end;

theorem Th42: :: YELLOW20:42

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂ st b₃ is bijective holds
b₁,b₂ are_isomorphic_under b₃

proof end;

theorem Th43: :: YELLOW20:43

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂ st b₃ is bijective holds
b₁,b₂ are_anti-isomorphic_under b₃

proof end;

scheme :: YELLOW20:sch 4
s4{ F₁() -> non empty category, F₂() -> non empty category, F₃() -> covariant Functor of F₁(),F₂(), F₄() -> non empty subcategory of F₁(), F₅() -> non empty subcategory of F₂() } :

F₄(),F₅() are_isomorphic_under F₃()

provided

E32: F₃() is bijective and
E33: for b₁ being object of F₁() holds
( b₁ is object of F₄() iff F₃() . b₁ is object of F₅() ) and
E34: for b₁, b₂ being object of F₁() st <^b₁,b₂^> <> {} holds
for b₃, b₄ being object of F₄() st b₃ = b₁ & b₄ = b₂ holds
for b₅, b₆ being object of F₅() st b₅ = F₃() . b₁ & b₆ = F₃() . b₂ holds
for b₇ being Morphism of b₁,b₂ holds
( b₇ in <^b₃,b₄^> iff F₃() . b₇ in <^b₅,b₆^> )

proof end;

scheme :: YELLOW20:sch 5
s5{ F₁() -> non empty category, F₂() -> non empty category, F₃() -> contravariant Functor of F₁(),F₂(), F₄() -> non empty subcategory of F₁(), F₅() -> non empty subcategory of F₂() } :

F₄(),F₅() are_anti-isomorphic_under F₃()

provided

proof end;

theorem Th44: :: YELLOW20:44

for b₁ being category
for b₂ being non empty subcategory of b₁ holds b₂,b₂ are_isomorphic_under id b₁

proof end;

theorem Th45: :: YELLOW20:45

for b₁, b₂ being Function st b₁ c= b₂ holds
~ b₁ c= ~ b₂

proof end;

theorem Th46: :: YELLOW20:46

for b₁, b₂ being Function st dom b₁ is Relation & ~ b₁ c= ~ b₂ holds
b₁ c= b₂

proof end;

theorem Th47: :: YELLOW20:47

for b₁, b₂ being set
for b₃ being ManySortedSet of [:b₁,b₁:]
for b₄ being ManySortedSet of [:b₂,b₂:] st b₃ cc= b₄ holds
~ b₃ cc= ~ b₄

proof end;

theorem Th48: :: YELLOW20:48

for b₁ being non empty transitive AltCatStr
for b₂ being non empty transitive SubCatStr of b₁ holds b₂ opp is SubCatStr of b₁ opp

proof end;

theorem Th49: :: YELLOW20:49

for b₁ being category
for b₂ being non empty subcategory of b₁ holds b₂ opp is subcategory of b₁ opp

proof end;

theorem Th50: :: YELLOW20:50

for b₁ being category
for b₂ being non empty subcategory of b₁ holds b₂,b₂ opp are_anti-isomorphic_under dualizing-func b₁,(b₁ opp )

proof end;

theorem Th51: :: YELLOW20:51

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being non empty subcategory of b₁
for b₅ being non empty subcategory of b₂ st b₄,b₅ are_isomorphic_under b₃ holds
b₅,b₄ are_isomorphic_under b₃ "

proof end;

theorem Th52: :: YELLOW20:52

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂ st b₃ is bijective holds
for b₄ being non empty subcategory of b₁
for b₅ being non empty subcategory of b₂ st b₄,b₅ are_anti-isomorphic_under b₃ holds
b₅,b₄ are_anti-isomorphic_under b₃ "

proof end;

theorem Th53: :: YELLOW20:53

for b₁, b₂, b₃ being category
for b₄ being covariant Functor of b₁,b₂
for b₅ being covariant Functor of b₂,b₃
for b₆ being non empty subcategory of b₁
for b₇ being non empty subcategory of b₂
for b₈ being non empty subcategory of b₃ st b₆,b₇ are_isomorphic_under b₄ & b₇,b₈ are_isomorphic_under b₅ holds
b₆,b₈ are_isomorphic_under b₅ * b₄

proof end;

theorem Th54: :: YELLOW20:54

for b₁, b₂, b₃ being category
for b₄ being contravariant Functor of b₁,b₂
for b₅ being covariant Functor of b₂,b₃
for b₆ being non empty subcategory of b₁
for b₇ being non empty subcategory of b₂
for b₈ being non empty subcategory of b₃ st b₆,b₇ are_anti-isomorphic_under b₄ & b₇,b₈ are_isomorphic_under b₅ holds
b₆,b₈ are_anti-isomorphic_under b₅ * b₄

proof end;

theorem Th55: :: YELLOW20:55

for b₁, b₂, b₃ being category
for b₄ being covariant Functor of b₁,b₂
for b₅ being contravariant Functor of b₂,b₃
for b₆ being non empty subcategory of b₁
for b₇ being non empty subcategory of b₂
for b₈ being non empty subcategory of b₃ st b₆,b₇ are_isomorphic_under b₄ & b₇,b₈ are_anti-isomorphic_under b₅ holds
b₆,b₈ are_anti-isomorphic_under b₅ * b₄

proof end;

theorem Th56: :: YELLOW20:56

for b₁, b₂, b₃ being category
for b₄ being contravariant Functor of b₁,b₂
for b₅ being contravariant Functor of b₂,b₃
for b₆ being non empty subcategory of b₁
for b₇ being non empty subcategory of b₂
for b₈ being non empty subcategory of b₃ st b₆,b₇ are_anti-isomorphic_under b₄ & b₇,b₈ are_anti-isomorphic_under b₅ holds
b₆,b₈ are_isomorphic_under b₅ * b₄

proof end;