let A1, A2, A3 be category; :: thesis: for F being contravariant Functor of A1,A2
for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of non empty
for B2 being non empty subcategory of non empty
for B3 being non empty subcategory of non empty st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let F be contravariant Functor of A1,A2; :: thesis: for G being contravariant Functor of A2,A3
for B1 being non empty subcategory of non empty
for B2 being non empty subcategory of non empty
for B3 being non empty subcategory of non empty st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let G be contravariant Functor of A2,A3; :: thesis: for B1 being non empty subcategory of non empty
for B2 being non empty subcategory of non empty
for B3 being non empty subcategory of non empty st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B1 be non empty subcategory of non empty ; :: thesis: for B2 being non empty subcategory of non empty
for B3 being non empty subcategory of non empty st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B2 be non empty subcategory of non empty ; :: thesis: for B3 being non empty subcategory of non empty st B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G holds
B1,B3 are_isomorphic_under G * F
let B3 be non empty subcategory of non empty ; :: thesis: ( B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G implies B1,B3 are_isomorphic_under G * F )
assume that
B1 is subcategory of and
B2 is subcategory of ; :: according to YELLOW20:def 5 :: thesis: ( for G being contravariant 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 not B2,B3 are_anti-isomorphic_under G or B1,B3 are_isomorphic_under G * F )
given F1 being contravariant Functor of B1,B2 such that A1: F1 is bijective and
A2: for a being object of
for a1 being object of st a = a1 holds
F1 . a = F . a1 and
A3: 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
F1 . f = (Morph-Map F,b1,c1) . f1 ; :: thesis: ( not B2,B3 are_anti-isomorphic_under G or B1,B3 are_isomorphic_under G * F )
assume that
B2 is subcategory of and
B3 is subcategory of ; :: according to YELLOW20:def 5 :: thesis: ( for G being contravariant Functor of B2,B3 holds
( not G is bijective or ex a' being object of ex a being object of st
( a' = a & not G . a' = G . 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 G,b,c) . f ) ) ) or B1,B3 are_isomorphic_under G * F )
given G1 being contravariant Functor of B2,B3 such that A4: G1 is bijective and
A5: for a being object of
for a1 being object of st a = a1 holds
G1 . a = G . a1 and
A6: 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
G1 . f = (Morph-Map G,b1,c1) . f1 ; :: thesis: B1,B3 are_isomorphic_under G * F
thus ( B1 is subcategory of & B3 is subcategory of ) ; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of B1,B3 st
( G is bijective & ( for a' being object of
for a being object of st a' = a holds
G . a' = (G * 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 (G * F),b,c) . f ) )
take G1 * F1 ; :: thesis: ( G1 * F1 is bijective & ( for a' being object of
for a being object of st a' = a holds
(G1 * F1) . a' = (G * 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
(G1 * F1) . f' = (Morph-Map (G * F),b,c) . f ) )
thus G1 * F1 is bijective by A1, A4, FUNCTOR1:13; :: thesis: ( ( for a' being object of
for a being object of st a' = a holds
(G1 * F1) . a' = (G * 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
(G1 * F1) . f' = (Morph-Map (G * F),b,c) . f ) )

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
(G1 * F1) . f' = (Morph-Map (G * F),b,c) . f

let a be object of ; :: thesis: for b being object of st a = b holds
(G1 * F1) . a = (G * F) . b
let b be object of ; :: thesis: ( a = b implies (G1 * F1) . a = (G * F) . b )
assume a = b ; :: thesis: (G1 * F1) . a = (G * F) . b
then G1 . (F1 . a) = G . (F . b) by A2, A5;
hence (G1 * F1) . a = G . (F . b) by FUNCTOR0:34
.= (G * F) . b by FUNCTOR0:34 ;
:: 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
(G1 * F1) . f' = (Morph-Map (G * 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
(G1 * F1) . f' = (Morph-Map (G * F),b1,c1) . f )
assume that
A7: <^b,c^> <> {} and
A8: ( b = b1 & c = c1 ) ; :: thesis: for f' being Morphism of ,
for f being Morphism of , st f' = f holds
(G1 * F1) . f' = (Morph-Map (G * F),b1,c1) . f
A9: ( (G * F) . b1 = G . (F . b1) & (G * F) . c1 = G . (F . c1) ) by FUNCTOR0:34;
let f be Morphism of ,; :: thesis: for f being Morphism of , st f = f holds
(G1 * F1) . f = (Morph-Map (G * F),b1,c1) . f
let f1 be Morphism of ,; :: thesis: ( f = f1 implies (G1 * F1) . f = (Morph-Map (G * F),b1,c1) . f1 )
A10: ( f in <^b,c^> & <^b,c^> c= <^b1,c1^> ) by A7, A8, ALTCAT_2:32;
then A11: <^((G * F) . b1),((G * F) . c1)^> <> {} by FUNCTOR0:def 19;
A12: <^(F1 . c),(F1 . b)^> <> {} by A7, FUNCTOR0:def 20;
then A13: F1 . f in <^(F1 . c),(F1 . b)^> ;
A14: ( F1 . b = F . b1 & F1 . c = F . c1 ) by A2, A8;
then A15: <^(F1 . c),(F1 . b)^> c= <^(F . c1),(F . b1)^> by ALTCAT_2:32;
assume f = f1 ; :: thesis: (G1 * F1) . f = (Morph-Map (G * F),b1,c1) . f1
then F1 . f = (Morph-Map F,b1,c1) . f1 by A3, A7, A8
.= F . f1 by A10, A13, A15, FUNCTOR0:def 17 ;
then G1 . (F1 . f) = (Morph-Map G,(F . c1),(F . b1)) . (F . f1) by A6, A12, A14;
hence (G1 * F1) . f = (Morph-Map G,(F . c1),(F . b1)) . (F . f1) by A7, FUNCTOR3:7
.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def 17
.= (G * F) . f1 by A10, FUNCTOR3:7
.= (Morph-Map (G * F),b1,c1) . f1 by A10, A11, FUNCTOR0:def 16 ;
:: thesis: verum