theorem
for
A1,
A2 being
category for
F being
covariant Functor of
A1,
A2 for
B1 being non
empty subcategory of
A1 for
B2 being non
empty subcategory of
A2 st
F is
bijective & ( for
a being
Object of
A1 holds
(
a is
Object of
B1 iff
F . a is
Object of
B2 ) ) & ( for
a,
b being
Object of
A1 st
<^a,b^> <> {} holds
for
a1,
b1 being
Object of
B1 st
a1 = a &
b1 = b holds
for
a2,
b2 being
Object of
B2 st
a2 = F . a &
b2 = F . b holds
for
f being
Morphism of
a,
b holds
(
f in <^a1,b1^> iff
F . f in <^a2,b2^> ) ) holds
B1,
B2 are_isomorphic_under F