let A, B be category; :: thesis: for F being covariant Functor of A,B st F is bijective holds
A,B are_isomorphic_under F
let F be covariant Functor of A,B; :: thesis: ( F is bijective implies A,B are_isomorphic_under F )
assume A1: F is bijective ; :: thesis: A,B are_isomorphic_under F
( the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B ) ;
hence ( A is subcategory of A & B is subcategory of B ) by ALTCAT_2:20, ALTCAT_4:35; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of A,B st
( G is bijective & ( for a9, a being Object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9, b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f ) )
take F ; :: thesis: ( F is bijective & ( for a9, a being Object of A st a9 = a holds
F . a9 = F . a ) & ( for b9, c9, b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f ) )
thus ( F is bijective & ( for a9, a being Object of A st a9 = a holds
F . a9 = F . a ) ) by A1; :: thesis: for b9, c9, b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f
let b9, c9 be Object of A; :: thesis: for b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f
let b, c be Object of A; :: thesis: ( <^b9,c9^> <> {} & b9 = b & c9 = c implies for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f )
assume A2: ( <^b9,c9^> <> {} & b9 = b & c9 = c ) ; :: thesis: for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f
then <^(F . b),(F . c)^> <> {} by FUNCTOR0:def 18;
hence for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
F . f9 = (Morph-Map (F,b,c)) . f by A2, FUNCTOR0:def 15; :: thesis: verum