let A, B be category; :: thesis: for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds
F is bijective
let F be contravariant Functor of A,B; :: thesis: ( A,B are_anti-isomorphic_under F implies F is bijective )
assume ( A is subcategory of A & B is subcategory of B ) ; :: according to YELLOW20:def 5 :: thesis: ( for G being contravariant Functor of A,B holds
( not G is bijective or ex a', a being object of A st
( a' = a & not G . a' = F . a ) or ex b', c', b, c being object of A st
( <^b',c'^> <> {} & b' = b & c' = c & ex f' being Morphism of b',c' ex f being Morphism of b,c st
( f' = f & not G . f' = (Morph-Map F,b,c) . f ) ) ) or F is bijective )
given G being contravariant Functor of A,B such that A1: G is bijective and
A2: for a', a being object of A st a' = a holds
G . a' = F . a and
A3: for b', c', b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
G . f' = (Morph-Map F,b,c) . f ; :: thesis: F is bijective
A4: for a being object of A holds F . a = G . a by A2;

now

let a, b be object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )
assume A5: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = G . f
let f be Morphism of a,b; :: thesis: F . f = G . f
<^(F . b),(F . a)^> <> {} by A5, FUNCTOR0:def 20;
hence F . f = (Morph-Map F,a,b) . f by A5, FUNCTOR0:def 17
.= G . f by A3, A5 ;
:: thesis: verum

end;

then A6: FunctorStr(# the ObjectMap of F,the MorphMap of F #) = FunctorStr(# the ObjectMap of G,the MorphMap of G #) by A4, YELLOW18:2;
( G is injective & G is surjective ) by A1, FUNCTOR0:def 36;
then ( G is one-to-one & G is faithful & G is full & G is onto ) by FUNCTOR0:def 34, FUNCTOR0:def 35;
hence ( the ObjectMap of F is one-to-one & the MorphMap of F is "1-1" & ex f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) & the ObjectMap of F is onto ) by A6, FUNCTOR0:def 7, FUNCTOR0:def 8, FUNCTOR0:def 31, FUNCTOR0:def 33; :: according to FUNCTOR0:def 7,FUNCTOR0:def 8,FUNCTOR0:def 31,FUNCTOR0:def 33,FUNCTOR0:def 34,FUNCTOR0:def 35,FUNCTOR0:def 36 :: thesis: verum