let A1, A2 be category; :: thesis: for F being covariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of non empty
for B2 being non empty subcategory of non empty st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
let F be covariant Functor of A1,A2; :: thesis: ( F is bijective implies for B1 being non empty subcategory of non empty
for B2 being non empty subcategory of non empty st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F " )
assume A1: F is bijective ; :: thesis: for B1 being non empty subcategory of non empty
for B2 being non empty subcategory of non empty st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
F is surjective by A1, FUNCTOR0:def 36;
then F is onto by FUNCTOR0:def 35;
then A2: F is coreflexive by FUNCTOR0:47;
ex H being Functor of A2,A1 st
( H = F " & H is bijective & H is covariant ) by A1, FUNCTOR0:49;
then reconsider F' = F " as covariant Functor of A2,A1 ;
let B1 be non empty subcategory of non empty ; :: thesis: for B2 being non empty subcategory of non empty st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
let B2 be non empty subcategory of non empty ; :: thesis: ( B1,B2 are_isomorphic_under F implies B2,B1 are_isomorphic_under F " )
assume that
B1 is subcategory of and
B2 is subcategory of ; :: according to YELLOW20:def 4 :: thesis: ( for G being covariant Functor of B1,B2 holds
( not G is bijective or ex a' being object of ex a being object of st
( a' = a & not G . a' = F . a ) or ex b', c' being object of ex b, c being object of st
( <^b',c'^> <> {} & b' = b & c' = c & ex f' being Morphism of , ex f being Morphism of , st
( f' = f & not G . f' = (Morph-Map F,b,c) . f ) ) ) or B2,B1 are_isomorphic_under F " )
given G being covariant Functor of B1,B2 such that A3: G is bijective and
A4: for a being object of
for a1 being object of st a = a1 holds
G . a = F . a1 and
A5: for b, c being object of
for b1, c1 being object of st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of ,
for f1 being Morphism of , st f = f1 holds
G . f = (Morph-Map F,b1,c1) . f1 ; :: thesis: B2,B1 are_isomorphic_under F "
G is surjective by A3, FUNCTOR0:def 36;
then G is onto by FUNCTOR0:def 35;
then A6: G is coreflexive by FUNCTOR0:47;
thus ( B2 is subcategory of & B1 is subcategory of ) ; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of B2,B1 st
( G is bijective & ( for a' being object of
for a being object of st a' = a holds
G . a' = (F " ) . a ) & ( for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (F " ),b,c) . f ) )
consider H being Functor of B2,B1 such that
A7: H = G " and
A8: ( H is bijective & H is covariant ) by A3, FUNCTOR0:49;
reconsider H = H as covariant Functor of B2,B1 by A8;
take H ; :: thesis: ( H is bijective & ( for a' being object of
for a being object of st a' = a holds
H . a' = (F " ) . a ) & ( for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
H . f' = (Morph-Map (F " ),b,c) . f ) )
thus H is bijective by A8; :: thesis: ( ( for a' being object of
for a being object of st a' = a holds
H . a' = (F " ) . a ) & ( for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
H . f' = (Morph-Map (F " ),b,c) . f ) )
A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

hereby :: thesis: for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
H . f' = (Morph-Map (F " ),b,c) . f

let a be object of ; :: thesis: for a1 being object of st a = a1 holds
H . a = (F " ) . a1
let a1 be object of ; :: thesis: ( a = a1 implies H . a = (F " ) . a1 )
H . a in the carrier of B1 ;
then reconsider Ha = H . a as object of by A9;
G . (H . a) = F . Ha by A4;
then A11: F . Ha = a by A3, A7, A6, Th1;
assume a = a1 ; :: thesis: H . a = (F " ) . a1
hence H . a = (F " ) . a1 by A1, A2, A11, Th1; :: thesis: verum

end;

let b, c be object of ; :: thesis: for b, c being object of st <^b,c^> <> {} & b = b & c = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
H . f' = (Morph-Map (F " ),b,c) . f
let b1, c1 be object of ; :: thesis: ( <^b,c^> <> {} & b = b1 & c = c1 implies for f' being Morphism of ,
for f being Morphism of , st f' = f holds
H . f' = (Morph-Map (F " ),b1,c1) . f )
assume that
A12: <^b,c^> <> {} and
A13: ( b = b1 & c = c1 ) ; :: thesis: for f' being Morphism of ,
for f being Morphism of , st f' = f holds
H . f' = (Morph-Map (F " ),b1,c1) . f
let f be Morphism of ,; :: thesis: for f being Morphism of , st f = f holds
H . f = (Morph-Map (F " ),b1,c1) . f
let f1 be Morphism of ,; :: thesis: ( f = f1 implies H . f = (Morph-Map (F " ),b1,c1) . f1 )
assume A14: f = f1 ; :: thesis: H . f = (Morph-Map (F " ),b1,c1) . f1
A15: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A12, A13, ALTCAT_2:32;
A16: ( G . (H . b) = b & G . (H . c) = c ) by A3, A7, A6, Th1;
A17: <^(H . b),(H . c)^> <> {} by A12, FUNCTOR0:def 19;
then A18: H . f in <^(H . b),(H . c)^> ;
A19: ( F . ((F " ) . b1) = b1 & F . ((F " ) . c1) = c1 ) by A1, A2, Th1;
A20: ( H . b = (F " ) . b1 & H . c = (F " ) . c1 ) by A10, A13;
then A21: <^(H . b),(H . c)^> c= <^((F " ) . b1),((F " ) . c1)^> by ALTCAT_2:32;
then reconsider Hf = H . f as Morphism of , by A18;
G . (H . f) = (Morph-Map F,((F " ) . b1),((F " ) . c1)) . Hf by A5, A20, A17
.= F . Hf by A21, A18, A15, A19, FUNCTOR0:def 16 ;
then F . Hf = f by A3, A7, A17, A16, Th2;
hence H . f = F' . f1 by A1, A14, A21, A18, A19, Th2
.= (Morph-Map (F " ),b1,c1) . f1 by A21, A18, A15, FUNCTOR0:def 16 ;
:: thesis: verum