let A, B, A9, B9 be category; :: thesis: for F being FunctorStr of A,B st A9,B9 are_isomorphic_under F holds
A9,B9 are_isomorphic
let F be FunctorStr of A,B; :: thesis: ( A9,B9 are_isomorphic_under F implies A9,B9 are_isomorphic )
assume that
A9 is subcategory of A and
B9 is subcategory of B ; :: according to YELLOW20:def 4 :: thesis: ( for G being covariant Functor of A9,B9 holds
( not G is bijective or ex a9 being object of A9 ex a being object of A st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being object of A9 ex b, c being object of A st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or A9,B9 are_isomorphic )
given G being covariant Functor of A9,B9 such that A1: G is bijective and
for a9 being object of A9
for a being object of A st a9 = a holds
G . a9 = F . a and
for b9, c9 being object of A9
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
G . f9 = (Morph-Map (F,b,c)) . f ; :: thesis: A9,B9 are_isomorphic
take G ; :: according to FUNCTOR0:def 39 :: thesis: ( G is bijective & G is covariant )
thus ( G is bijective & G is covariant ) by A1; :: thesis: verum