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 H1( 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 H2( Element of H1(B), Element of H1(C)) -> Element of the carrier' of D = ((L . (cod \$2)) . \$1) (*) ((M . (dom \$1)) . \$2);
consider S being Function of [:H1(B),H1(C):],H1(D) such that
A3: for f being Morphism of B
for g being Morphism of C holds S . (f,g) = H2(f,g) from reconsider T = S as Function of H1([:B,C:]),H1(D) ;
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) ) )
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) ) )
proof
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 ; :: thesis: verum
end;
thus for fg being Morphism of [:B,C:] holds
( 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 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
.= 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
.= id (dom (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by
.= 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
.= 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
.= id (cod (((L . (cod g)) . f) (*) ((M . (dom f)) . g))) by
.= id (cod (S . (f,g))) by A3
.= id (cod (T . fg)) by A8 ; :: thesis: verum
end;
let fg1, fg2 be Morphism of [:B,C:]; :: thesis: ( dom fg2 = cod fg1 implies 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 ;
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 ;
then A17: dom f2 = cod f1 by ;
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 ;
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
.= ((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
.= ((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by
.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) ((M . (dom f1)) . (g2 (*) g1)) by
.= (((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) by
.= ((L . (cod g2)) . f2) (*) (((L . (cod g2)) . f1) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1))) by
.= ((L . (cod g2)) . f2) (*) ((((L . (cod g2)) . f1) (*) ((M . (dom f1)) . g2)) (*) ((M . (dom f1)) . g1)) by
.= ((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
.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) by
.= (((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (S . (f1,g1)) by A3
.= (S . (f2,g2)) (*) (T . fg1) by
.= (T . fg2) (*) (T . fg1) by A14 ; :: thesis: verum
end;
then reconsider T = T as Functor of [:B,C:],D by CAT_1:61;
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