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₁( 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₂( Element of H₁(B), Element of H₁(C)) -> Element of the carrier' of D = ((L . (cod $2)) . $1) (*) ((M . (dom $1)) . $2);
consider S being Function of [:H₁(B),H₁(C):],H₁(D) such that
A3: for f being Morphism of B
for g being Morphism of C holds S . (f,g) = H₂(f,g) from BINOP_1:sch 4();
reconsider T = S as Function of H₁([:B,C:]),H₁(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 A4, Th25; :: 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 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;

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 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;

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