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

hereby :: thesis: for b9, c9 being Object of B1
for b, c being Object of A1 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
(G1 * F1) . f9 = (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:33
.= (G * F) . b by FUNCTOR0:33 ;
:: 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 f9 being Morphism of b,c
for f being Morphism of b,c st f9 = f holds
(G1 * F1) . f9 = (Morph-Map ((G * F),b,c)) . f
let b1, c1 be Object of A1; :: 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
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f )
assume that
A7: <^b,c^> <> {} and
A8: ( b = b1 & c = c1 ) ; :: thesis: for f9 being Morphism of b,c
for f being Morphism of b1,c1 st f9 = f holds
(G1 * F1) . f9 = (Morph-Map ((G * F),b1,c1)) . f
A9: ( (G * F) . b1 = G . (F . b1) & (G * F) . c1 = G . (F . c1) ) by FUNCTOR0:33;
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 )
A10: ( f in <^b,c^> & <^b,c^> c= <^b1,c1^> ) by A7, A8, ALTCAT_2:31;
then A11: <^((G * F) . c1),((G * F) . b1)^> <> {} by FUNCTOR0:def 19;
A12: <^(F1 . c),(F1 . b)^> <> {} by A7, FUNCTOR0:def 19;
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:31;
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 16 ;
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:9
.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def 15
.= (G * F) . f1 by A10, FUNCTOR3:9
.= (Morph-Map ((G * F),b1,c1)) . f1 by A10, A11, FUNCTOR0:def 16 ;
:: thesis: verum