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 A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 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 A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 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 A1
for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 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 A1; :: thesis: for B2 being non empty subcategory of A2
for B3 being non empty subcategory of A3 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 A2; :: thesis: for B3 being non empty subcategory of A3 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 A3; :: thesis: ( B1,B2 are_anti-isomorphic_under F & B2,B3 are_anti-isomorphic_under G implies B1,B3 are_isomorphic_under G * F )
assume ( B1 is subcategory of A1 & B2 is subcategory of A2 ) ; :: 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 B1 ex a being object of A1 st
( a' = a & not G . a' = F . a ) or ex b', c' being object of B1 ex b, c being object of A1 st
( <^b',c'^> <> {} & b' = b & c' = c & ex f' being Morphism of b',c' ex f being Morphism of b,c 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 B1
for a1 being object of A1 st a = a1 holds
F1 . a = F . a1 and
A3: 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
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 ( B2 is subcategory of A2 & B3 is subcategory of A3 ) ; :: 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 B2 ex a being object of A2 st
( a' = a & not G . a' = G . a ) or ex b', c' being object of B2 ex b, c being object of A2 st
( <^b',c'^> <> {} & b' = b & c' = c & ex f' being Morphism of b',c' ex f being Morphism of b,c 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 B2
for a1 being object of A2 st a = a1 holds
G1 . a = G . a1 and
A6: for b, c being object of B2
for b1, c1 being object of A2 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
G1 . f = (Morph-Map G,b1,c1) . f1 ; :: thesis: B1,B3 are_isomorphic_under G * F
thus ( B1 is subcategory of A1 & B3 is subcategory of A3 ) ; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of B1,B3 st
( G is bijective & ( for a' being object of B1
for a being object of A1 st a' = a holds
G . a' = (G * F) . a ) & ( for b', c' being object of B1
for b, c being object of A1 st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c 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 B1
for a being object of A1 st a' = a holds
(G1 * F1) . a' = (G * F) . a ) & ( for b', c' being object of B1
for b, c being object of A1 st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c 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 B1
for a being object of A1 st a' = a holds
(G1 * F1) . a' = (G * F) . a ) & ( for b', c' being object of B1
for b, c being object of A1 st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
(G1 * F1) . f' = (Morph-Map (G * F),b,c) . f ) )

hereby :: thesis: for b', c' being object of B1
for b, c being object of A1 st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
(G1 * F1) . f' = (Morph-Map (G * F),b,c) . f

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