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

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