let B, C, D be Category; :: thesis: for L being Function of the carrier of C,(Funct (B,D))

for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds

ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

deffunc H_{1}( Category) -> set = the carrier' of $1;

let L be Function of the carrier of C,(Funct (B,D)); :: thesis: for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds

ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

let M be Function of the carrier of B,(Funct (C,D)); :: thesis: ( ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) implies ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) )

assume that

A1: for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) and

A2: for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ; :: thesis: ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

deffunc H_{2}( Element of H_{1}(B), Element of H_{1}(C)) -> Element of the carrier' of D = ((L . (cod $2)) . $1) (*) ((M . (dom $1)) . $2);

consider S being Function of [:H_{1}(B),H_{1}(C):],H_{1}(D) such that

A3: for f being Morphism of B

for g being Morphism of C holds S . (f,g) = H_{2}(f,g)
from BINOP_1:sch 4();

reconsider T = S as Function of H_{1}([:B,C:]),H_{1}(D) ;

take T ; :: thesis: for f being Morphism of B

for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

thus for f being Morphism of B

for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A3; :: thesis: verum

for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds

ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

deffunc H

let L be Function of the carrier of C,(Funct (B,D)); :: thesis: for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds

ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

let M be Function of the carrier of B,(Funct (C,D)); :: thesis: ( ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) implies ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) )

assume that

A1: for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) and

A2: for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ; :: thesis: ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

deffunc H

consider S being Function of [:H

A3: for f being Morphism of B

for g being Morphism of C holds S . (f,g) = H

reconsider T = S as Function of H

now :: thesis: ( ( for bc being Object of [:B,C:] ex d being Object of D st T . (id bc) = id d ) & ( for fg being Morphism of [:B,C:] holds

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds

T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) )

then reconsider T = T as Functor of [:B,C:],D by CAT_1:61;( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds

T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) )

thus
for bc being Object of [:B,C:] ex d being Object of D st T . (id bc) = id d
:: thesis: ( ( for fg being Morphism of [:B,C:] holds

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds

T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) )

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis: for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds

T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)

assume A12: dom fg2 = cod fg1 ; :: thesis: T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)

consider f1 being Morphism of B, g1 being Morphism of C such that

A13: fg1 = [f1,g1] by DOMAIN_1:1;

consider f2 being Morphism of B, g2 being Morphism of C such that

A14: fg2 = [f2,g2] by DOMAIN_1:1;

A15: [(cod f1),(cod g1)] = cod fg1 by A13, Th22;

set L1 = L . (cod g1);

set L2 = L . (cod g2);

set M1 = M . (dom f1);

set M2 = M . (dom f2);

A16: [(dom f2),(dom g2)] = dom fg2 by A14, Th22;

then A17: dom f2 = cod f1 by A12, A15, XTUPLE_0:1;

then A18: dom ((L . (cod g2)) . f2) = cod ((L . (cod g2)) . f1) by CAT_1:64;

id (dom ((L . (cod g1)) . f1)) = (L . (cod g1)) . (id (dom f1)) by CAT_1:63

.= (M . (dom f1)) . (id (cod g1)) by A1

.= id (cod ((M . (dom f1)) . g1)) by CAT_1:63 ;

then A19: dom ((L . (cod g1)) . f1) = cod ((M . (dom f1)) . g1) by CAT_1:59;

then A20: cod (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) = cod ((L . (cod g1)) . f1) by CAT_1:17;

A21: dom g2 = cod g1 by A12, A16, A15, XTUPLE_0:1;

then A22: dom ((M . (dom f1)) . g2) = cod ((M . (dom f1)) . g1) by CAT_1:64;

then A23: cod (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) = cod ((M . (dom f1)) . g2) by CAT_1:17;

id (dom ((M . (dom f2)) . g2)) = (M . (dom f2)) . (id (dom g2)) by CAT_1:63

.= (L . (cod g1)) . (id (cod f1)) by A1, A17, A21

.= id (cod ((L . (cod g1)) . f1)) by CAT_1:63 ;

then A24: dom ((M . (dom f2)) . g2) = cod ((L . (cod g1)) . f1) by CAT_1:59;

id (dom ((L . (cod g2)) . f2)) = (L . (cod g2)) . (id (dom f2)) by CAT_1:63

.= (M . (dom f2)) . (id (cod g2)) by A1

.= id (cod ((M . (dom f2)) . g2)) by CAT_1:63 ;

then A25: dom ((L . (cod g2)) . f2) = cod ((M . (dom f2)) . g2) by CAT_1:59;

set f = f2 (*) f1;

set g = g2 (*) g1;

id (dom ((L . (cod g2)) . f1)) = (L . (cod g2)) . (id (dom f1)) by CAT_1:63

.= (M . (dom f1)) . (id (cod g2)) by A1

.= id (cod ((M . (dom f1)) . g2)) by CAT_1:63 ;

then A26: dom ((L . (cod g2)) . f1) = cod ((M . (dom f1)) . g2) by CAT_1:59;

thus T . (fg2 (*) fg1) = S . ((f2 (*) f1),(g2 (*) g1)) by A12, A13, A14, Th24

.= ((L . (cod (g2 (*) g1))) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A3

.= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A21, CAT_1:17

.= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:17

.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:64

.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) by A21, CAT_1:64

.= ((L . (cod g2)) . f2) (*) (((L . (cod g2)) . f1) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1))) by A18, A23, A26, CAT_1:18

.= ((L . (cod g2)) . f2) (*) ((((L . (cod g2)) . f1) (*) ((M . (dom f1)) . g2)) (*) ((M . (dom f1)) . g1)) by A22, A26, CAT_1:18

.= ((L . (cod g2)) . f2) (*) ((((M . (dom f2)) . g2) (*) ((L . (cod g1)) . f1)) (*) ((M . (dom f1)) . g1)) by A2, A17, A21

.= ((L . (cod g2)) . f2) (*) (((M . (dom f2)) . g2) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1))) by A19, A24, CAT_1:18

.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) by A24, A25, A20, CAT_1:18

.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (S . (f1,g1)) by A3

.= (S . (f2,g2)) (*) (T . fg1) by A3, A13

.= (T . fg2) (*) (T . fg1) by A14 ; :: thesis: verum

end;( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds

T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) )

proof

thus
for fg being Morphism of [:B,C:] holds
let bc be Object of [:B,C:]; :: thesis: ex d being Object of D st T . (id bc) = id d

consider b being Object of B, c being Object of C such that

A4: bc = [b,c] by DOMAIN_1:1;

consider d being Object of D such that

A5: (L . c) . (id b) = id d by CAT_1:62;

take d ; :: thesis: T . (id bc) = id d

Hom (d,d) <> {} ;

then A6: (id d) * (id d) = (id d) (*) (id d) by CAT_1:def 13;

A7: ( cod (id c) = c & dom (id b) = b ) ;

(L . c) . (id b) = (M . b) . (id c) by A1;

then T . ((id b),(id c)) = id d by A3, A5, A6, A7;

hence T . (id bc) = id d by A4, Th25; :: thesis: verum

end;consider b being Object of B, c being Object of C such that

A4: bc = [b,c] by DOMAIN_1:1;

consider d being Object of D such that

A5: (L . c) . (id b) = id d by CAT_1:62;

take d ; :: thesis: T . (id bc) = id d

Hom (d,d) <> {} ;

then A6: (id d) * (id d) = (id d) (*) (id d) by CAT_1:def 13;

A7: ( cod (id c) = c & dom (id b) = b ) ;

(L . c) . (id b) = (M . b) . (id c) by A1;

then T . ((id b),(id c)) = id d by A3, A5, A6, A7;

hence T . (id bc) = id d by A4, Th25; :: thesis: verum

( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) :: thesis: for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds

T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)

proof

let fg1, fg2 be Morphism of [:B,C:]; :: thesis: ( dom fg2 = cod fg1 implies T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) )
let fg be Morphism of [:B,C:]; :: thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )

consider f being Morphism of B, g being Morphism of C such that

A8: fg = [f,g] by DOMAIN_1:1;

set b = dom f;

set c = dom g;

set g9 = id (dom g);

set f9 = id (dom f);

A9: Hom ((dom ((M . (dom f)) . g)),(dom ((M . (dom f)) . g))) <> {} ;

id (dom ((L . (cod g)) . f)) = (L . (cod g)) . (id (dom f)) by CAT_1:63

.= (M . (dom f)) . (id (cod g)) by A1

.= id (cod ((M . (dom f)) . g)) by CAT_1:63 ;

then A10: dom ((L . (cod g)) . f) = cod ((M . (dom f)) . g) by CAT_1:59;

thus T . (id (dom fg)) = S . (id [(dom f),(dom g)]) by A8, Th22

.= S . ((id (dom f)),(id (dom g))) by Th25

.= ((L . (cod (id (dom g)))) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g))) by A3

.= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g)))

.= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom f)) . (id (dom g)))

.= ((M . (dom f)) . (id (dom g))) (*) ((M . (dom f)) . (id (dom g))) by A1

.= (id (dom ((M . (dom f)) . g))) (*) ((M . (dom f)) . (id (dom g))) by CAT_1:63

.= (id (dom ((M . (dom f)) . g))) (*) (id (dom ((M . (dom f)) . g))) by CAT_1:63

.= (id (dom ((M . (dom f)) . g))) * (id (dom ((M . (dom f)) . g))) by A9, CAT_1:def 13

.= id (dom (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17

.= id (dom (S . (f,g))) by A3

.= id (dom (T . fg)) by A8 ; :: thesis: T . (id (cod fg)) = id (cod (T . fg))

set b = cod f;

set c = cod g;

set g9 = id (cod g);

set f9 = id (cod f);

A11: Hom ((cod ((L . (cod g)) . f)),(cod ((L . (cod g)) . f))) <> {} ;

thus T . (id (cod fg)) = S . (id [(cod f),(cod g)]) by A8, Th22

.= S . ((id (cod f)),(id (cod g))) by Th25

.= ((L . (cod (id (cod g)))) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g))) by A3

.= ((L . (cod g)) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g)))

.= ((L . (cod g)) . (id (cod f))) (*) ((M . (cod f)) . (id (cod g)))

.= ((L . (cod g)) . (id (cod f))) (*) ((L . (cod g)) . (id (cod f))) by A1

.= (id (cod ((L . (cod g)) . f))) (*) ((L . (cod g)) . (id (cod f))) by CAT_1:63

.= (id (cod ((L . (cod g)) . f))) (*) (id (cod ((L . (cod g)) . f))) by CAT_1:63

.= (id (cod ((L . (cod g)) . f))) * (id (cod ((L . (cod g)) . f))) by A11, CAT_1:def 13

.= id (cod (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17

.= id (cod (S . (f,g))) by A3

.= id (cod (T . fg)) by A8 ; :: thesis: verum

end;consider f being Morphism of B, g being Morphism of C such that

A8: fg = [f,g] by DOMAIN_1:1;

set b = dom f;

set c = dom g;

set g9 = id (dom g);

set f9 = id (dom f);

A9: Hom ((dom ((M . (dom f)) . g)),(dom ((M . (dom f)) . g))) <> {} ;

id (dom ((L . (cod g)) . f)) = (L . (cod g)) . (id (dom f)) by CAT_1:63

.= (M . (dom f)) . (id (cod g)) by A1

.= id (cod ((M . (dom f)) . g)) by CAT_1:63 ;

then A10: dom ((L . (cod g)) . f) = cod ((M . (dom f)) . g) by CAT_1:59;

thus T . (id (dom fg)) = S . (id [(dom f),(dom g)]) by A8, Th22

.= S . ((id (dom f)),(id (dom g))) by Th25

.= ((L . (cod (id (dom g)))) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g))) by A3

.= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g)))

.= ((L . (dom g)) . (id (dom f))) (*) ((M . (dom f)) . (id (dom g)))

.= ((M . (dom f)) . (id (dom g))) (*) ((M . (dom f)) . (id (dom g))) by A1

.= (id (dom ((M . (dom f)) . g))) (*) ((M . (dom f)) . (id (dom g))) by CAT_1:63

.= (id (dom ((M . (dom f)) . g))) (*) (id (dom ((M . (dom f)) . g))) by CAT_1:63

.= (id (dom ((M . (dom f)) . g))) * (id (dom ((M . (dom f)) . g))) by A9, CAT_1:def 13

.= id (dom (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17

.= id (dom (S . (f,g))) by A3

.= id (dom (T . fg)) by A8 ; :: thesis: T . (id (cod fg)) = id (cod (T . fg))

set b = cod f;

set c = cod g;

set g9 = id (cod g);

set f9 = id (cod f);

A11: Hom ((cod ((L . (cod g)) . f)),(cod ((L . (cod g)) . f))) <> {} ;

thus T . (id (cod fg)) = S . (id [(cod f),(cod g)]) by A8, Th22

.= S . ((id (cod f)),(id (cod g))) by Th25

.= ((L . (cod (id (cod g)))) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g))) by A3

.= ((L . (cod g)) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g)))

.= ((L . (cod g)) . (id (cod f))) (*) ((M . (cod f)) . (id (cod g)))

.= ((L . (cod g)) . (id (cod f))) (*) ((L . (cod g)) . (id (cod f))) by A1

.= (id (cod ((L . (cod g)) . f))) (*) ((L . (cod g)) . (id (cod f))) by CAT_1:63

.= (id (cod ((L . (cod g)) . f))) (*) (id (cod ((L . (cod g)) . f))) by CAT_1:63

.= (id (cod ((L . (cod g)) . f))) * (id (cod ((L . (cod g)) . f))) by A11, CAT_1:def 13

.= id (cod (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by A10, CAT_1:17

.= id (cod (S . (f,g))) by A3

.= id (cod (T . fg)) by A8 ; :: thesis: verum

assume A12: dom fg2 = cod fg1 ; :: thesis: T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)

consider f1 being Morphism of B, g1 being Morphism of C such that

A13: fg1 = [f1,g1] by DOMAIN_1:1;

consider f2 being Morphism of B, g2 being Morphism of C such that

A14: fg2 = [f2,g2] by DOMAIN_1:1;

A15: [(cod f1),(cod g1)] = cod fg1 by A13, Th22;

set L1 = L . (cod g1);

set L2 = L . (cod g2);

set M1 = M . (dom f1);

set M2 = M . (dom f2);

A16: [(dom f2),(dom g2)] = dom fg2 by A14, Th22;

then A17: dom f2 = cod f1 by A12, A15, XTUPLE_0:1;

then A18: dom ((L . (cod g2)) . f2) = cod ((L . (cod g2)) . f1) by CAT_1:64;

id (dom ((L . (cod g1)) . f1)) = (L . (cod g1)) . (id (dom f1)) by CAT_1:63

.= (M . (dom f1)) . (id (cod g1)) by A1

.= id (cod ((M . (dom f1)) . g1)) by CAT_1:63 ;

then A19: dom ((L . (cod g1)) . f1) = cod ((M . (dom f1)) . g1) by CAT_1:59;

then A20: cod (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) = cod ((L . (cod g1)) . f1) by CAT_1:17;

A21: dom g2 = cod g1 by A12, A16, A15, XTUPLE_0:1;

then A22: dom ((M . (dom f1)) . g2) = cod ((M . (dom f1)) . g1) by CAT_1:64;

then A23: cod (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) = cod ((M . (dom f1)) . g2) by CAT_1:17;

id (dom ((M . (dom f2)) . g2)) = (M . (dom f2)) . (id (dom g2)) by CAT_1:63

.= (L . (cod g1)) . (id (cod f1)) by A1, A17, A21

.= id (cod ((L . (cod g1)) . f1)) by CAT_1:63 ;

then A24: dom ((M . (dom f2)) . g2) = cod ((L . (cod g1)) . f1) by CAT_1:59;

id (dom ((L . (cod g2)) . f2)) = (L . (cod g2)) . (id (dom f2)) by CAT_1:63

.= (M . (dom f2)) . (id (cod g2)) by A1

.= id (cod ((M . (dom f2)) . g2)) by CAT_1:63 ;

then A25: dom ((L . (cod g2)) . f2) = cod ((M . (dom f2)) . g2) by CAT_1:59;

set f = f2 (*) f1;

set g = g2 (*) g1;

id (dom ((L . (cod g2)) . f1)) = (L . (cod g2)) . (id (dom f1)) by CAT_1:63

.= (M . (dom f1)) . (id (cod g2)) by A1

.= id (cod ((M . (dom f1)) . g2)) by CAT_1:63 ;

then A26: dom ((L . (cod g2)) . f1) = cod ((M . (dom f1)) . g2) by CAT_1:59;

thus T . (fg2 (*) fg1) = S . ((f2 (*) f1),(g2 (*) g1)) by A12, A13, A14, Th24

.= ((L . (cod (g2 (*) g1))) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A3

.= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1)) by A21, CAT_1:17

.= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:17

.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by A17, CAT_1:64

.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) by A21, CAT_1:64

.= ((L . (cod g2)) . f2) (*) (((L . (cod g2)) . f1) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1))) by A18, A23, A26, CAT_1:18

.= ((L . (cod g2)) . f2) (*) ((((L . (cod g2)) . f1) (*) ((M . (dom f1)) . g2)) (*) ((M . (dom f1)) . g1)) by A22, A26, CAT_1:18

.= ((L . (cod g2)) . f2) (*) ((((M . (dom f2)) . g2) (*) ((L . (cod g1)) . f1)) (*) ((M . (dom f1)) . g1)) by A2, A17, A21

.= ((L . (cod g2)) . f2) (*) (((M . (dom f2)) . g2) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1))) by A19, A24, CAT_1:18

.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) by A24, A25, A20, CAT_1:18

.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (S . (f1,g1)) by A3

.= (S . (f2,g2)) (*) (T . fg1) by A3, A13

.= (T . fg2) (*) (T . fg1) by A14 ; :: thesis: verum

take T ; :: thesis: for f being Morphism of B

for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

thus for f being Morphism of B

for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A3; :: thesis: verum