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 A1
for B2 being non empty subcategory of A2 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 A1
for B2 being non empty subcategory of A2 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 A1
for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
F is surjective by A1;
then F is onto ;
then A2: F is coreflexive by FUNCTOR0:46;
ex H being Functor of A2,A1 st
( H = F " & H is bijective & H is covariant ) by A1, FUNCTOR0:48;
then reconsider F9 = F " as covariant Functor of A2,A1 ;
let B1 be non empty subcategory of A1; :: thesis: for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds
B2,B1 are_isomorphic_under F "
let B2 be non empty subcategory of A2; :: thesis: ( B1,B2 are_isomorphic_under F implies B2,B1 are_isomorphic_under F " )
assume that
B1 is subcategory of A1 and
B2 is subcategory of A2 ; :: according to YELLOW20:def 4 :: thesis: ( for G being covariant Functor of B1,B2 holds
( not G is bijective or ex a9 being Object of B1 ex a being Object of A1 st
( a9 = a & not G . a9 = F . a ) or ex b9, c9 being Object of B1 ex b, c being Object of A1 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 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 B1
for a1 being Object of A1 st a = a1 holds
G . a = F . a1 and
A5: for b, c being Object of B1
for b1, c1 being Object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G . f = (Morph-Map (F,b1,c1)) . f1 ; :: thesis: B2,B1 are_isomorphic_under F "
G is surjective by A3;
then G is onto ;
then A6: G is coreflexive by FUNCTOR0:46;
thus ( B2 is subcategory of A2 & B1 is subcategory of A1 ) ; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of B2,B1 st
( G is bijective & ( for a9 being Object of B2
for a being Object of A2 st a9 = a holds
G . a9 = (F ") . a ) & ( for b9, c9 being Object of B2
for b, c being Object of A2 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 ) )
consider H being Functor of B2,B1 such that
A7: H = G " and
A8: ( H is bijective & H is covariant ) by A3, FUNCTOR0:48;
reconsider H = H as covariant Functor of B2,B1 by A8;
take H ; :: thesis: ( H is bijective & ( for a9 being Object of B2
for a being Object of A2 st a9 = a holds
H . a9 = (F ") . a ) & ( for b9, c9 being Object of B2
for b, c being Object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f ) )
thus H is bijective by A8; :: thesis: ( ( for a9 being Object of B2
for a being Object of A2 st a9 = a holds
H . a9 = (F ") . a ) & ( for b9, c9 being Object of B2
for b, c being Object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f ) )
A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

hereby :: thesis: for b9, c9 being Object of B2
for b, c being Object of A2 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
H . f9 = (Morph-Map ((F "),b,c)) . f

let a be Object of B2; :: thesis: for a1 being Object of A2 st a = a1 holds
H . a = (F ") . a1
let a1 be Object of A2; :: thesis: ( a = a1 implies H . a = (F ") . a1 )
reconsider Ha = H . a as Object of A1 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 B2; :: thesis: for b, c being Object of A2 st <^b,c^> <> {} & b = b & c = c holds
for f9 being Morphism of b,c
for f being Morphism of b,c st f9 = f holds
H . f9 = (Morph-Map ((F "),b,c)) . f
let b1, c1 be Object of A2; :: thesis: ( <^b,c^> <> {} & b = b1 & c = c1 implies for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
H . f9 = (Morph-Map ((F "),b1,c1)) . f )
assume that
A12: <^b,c^> <> {} and
A13: ( b = b1 & c = c1 ) ; :: thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
H . f9 = (Morph-Map ((F "),b1,c1)) . f
let f be Morphism of b,c; :: thesis: for f being Morphism of b1,c1 st f = f holds
H . f = (Morph-Map ((F "),b1,c1)) . f
let f1 be Morphism of b1,c1; :: 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:31;
A16: ( G . (H . b) = b & G . (H . c) = c ) by A3, A7, A6, Th1;
A17: <^(H . b),(H . c)^> <> {} by A12, FUNCTOR0:def 18;
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:31;
then reconsider Hf = H . f as Morphism of ((F ") . b1),((F ") . c1) 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 15 ;
then F . Hf = f by A3, A7, A17, A16, Th2;
hence H . f = F9 . f1 by A1, A14, A21, A18, A19, Th2
.= (Morph-Map ((F "),b1,c1)) . f1 by A21, A18, A15, FUNCTOR0:def 15 ;
:: thesis: verum