let A1, A2, A3 be category; :: thesis: for F being covariant 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_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

let F be covariant 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_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_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_isomorphic_under F & B2,B3 are_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_isomorphic_under F & B2,B3 are_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_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

let B3 be non empty subcategory of A3; :: thesis: ( B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G implies B1,B3 are_isomorphic_under G * 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 not B2,B3 are_isomorphic_under G or B1,B3 are_isomorphic_under G * F )

given F1 being covariant 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_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_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_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 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 ) )

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) . b1),((G * F) . c1)^> <> {} by FUNCTOR0:def 18;

A12: <^(F1 . b),(F1 . c)^> <> {} by A7, FUNCTOR0:def 18;

then A13: F1 . f in <^(F1 . b),(F1 . c)^> ;

A14: ( F1 . b = F . b1 & F1 . c = F . c1 ) by A2, A8;

then A15: <^(F1 . b),(F1 . c)^> c= <^(F . b1),(F . c1)^> 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 15 ;

then G1 . (F1 . f) = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A6, A12, A14;

hence (G1 * F1) . f = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A7, FUNCTOR3:6

.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def 15

.= (G * F) . f1 by A10, FUNCTOR3:6

.= (Morph-Map ((G * F),b1,c1)) . f1 by A10, A11, FUNCTOR0:def 15 ;

:: thesis: verum

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_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

let F be covariant 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_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_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_isomorphic_under F & B2,B3 are_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_isomorphic_under F & B2,B3 are_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_isomorphic_under F & B2,B3 are_isomorphic_under G holds

B1,B3 are_isomorphic_under G * F

let B3 be non empty subcategory of A3; :: thesis: ( B1,B2 are_isomorphic_under F & B2,B3 are_isomorphic_under G implies B1,B3 are_isomorphic_under G * 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 not B2,B3 are_isomorphic_under G or B1,B3 are_isomorphic_under G * F )

given F1 being covariant 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_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_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_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 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 b, c be Object of B1; :: thesis: for b, c being Object of A1 st <^b,c^> <> {} & b = b & c = c holds 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;(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

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) . b1),((G * F) . c1)^> <> {} by FUNCTOR0:def 18;

A12: <^(F1 . b),(F1 . c)^> <> {} by A7, FUNCTOR0:def 18;

then A13: F1 . f in <^(F1 . b),(F1 . c)^> ;

A14: ( F1 . b = F . b1 & F1 . c = F . c1 ) by A2, A8;

then A15: <^(F1 . b),(F1 . c)^> c= <^(F . b1),(F . c1)^> 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 15 ;

then G1 . (F1 . f) = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A6, A12, A14;

hence (G1 * F1) . f = (Morph-Map (G,(F . b1),(F . c1))) . (F . f1) by A7, FUNCTOR3:6

.= G . (F . f1) by A13, A15, A11, A9, FUNCTOR0:def 15

.= (G * F) . f1 by A10, FUNCTOR3:6

.= (Morph-Map ((G * F),b1,c1)) . f1 by A10, A11, FUNCTOR0:def 15 ;

:: thesis: verum