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 ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) holds

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)

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 ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) holds

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)

let M be Function of the carrier of B,(Funct (C,D)); :: thesis: ( ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) implies 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) )

given S being Functor of [:B,C:],D such that A1: for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) ; :: thesis: 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)

let f be Morphism of B; :: thesis: for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

let g be Morphism of C; :: thesis: ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

dom (id (cod f)) = cod f ;

then A2: dom [(id (cod f)),g] = [(cod f),(dom g)] by Th22;

cod (id (dom g)) = dom g ;

then A3: cod [f,(id (dom g))] = [(cod f),(dom g)] by Th22;

cod (id (dom f)) = dom f ;

then A4: cod [(id (dom f)),g] = [(dom f),(cod g)] by Th22;

dom (id (cod g)) = cod g ;

then A5: dom [f,(id (cod g))] = [(dom f),(cod g)] by Th22;

thus ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((S ?- (cod f)) . g) (*) ((L . (dom g)) . f) by A1

.= ((S ?- (cod f)) . g) (*) ((S -? (dom g)) . f) by A1

.= (S . ((id (cod f)),g)) (*) ((S -? (dom g)) . f) by FUNCT_5:69

.= (S . ((id (cod f)),g)) (*) (S . (f,(id (dom g)))) by FUNCT_5:70

.= S . ([(id (cod f)),g] (*) [f,(id (dom g))]) by A2, A3, CAT_1:64

.= S . [((id (cod f)) (*) f),(g (*) (id (dom g)))] by A2, A3, Th24

.= S . [f,(g (*) (id (dom g)))] by CAT_1:21

.= S . [f,g] by CAT_1:22

.= S . [(f (*) (id (dom f))),g] by CAT_1:22

.= S . [(f (*) (id (dom f))),((id (cod g)) (*) g)] by CAT_1:21

.= S . ([f,(id (cod g))] (*) [(id (dom f)),g]) by A5, A4, Th24

.= (S . (f,(id (cod g)))) (*) (S . [(id (dom f)),g]) by A5, A4, CAT_1:64

.= ((S -? (cod g)) . f) (*) (S . ((id (dom f)),g)) by FUNCT_5:70

.= ((S -? (cod g)) . f) (*) ((S ?- (dom f)) . g) by FUNCT_5:69

.= ((L . (cod g)) . f) (*) ((S ?- (dom f)) . g) by A1

.= ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A1 ; :: thesis: verum

for M being Function of the carrier of B,(Funct (C,D)) st ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) holds

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)

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 ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) holds

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)

let M be Function of the carrier of B,(Funct (C,D)); :: thesis: ( ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) implies 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) )

given S being Functor of [:B,C:],D such that A1: for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) ; :: thesis: 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)

let f be Morphism of B; :: thesis: for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

let g be Morphism of C; :: thesis: ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

dom (id (cod f)) = cod f ;

then A2: dom [(id (cod f)),g] = [(cod f),(dom g)] by Th22;

cod (id (dom g)) = dom g ;

then A3: cod [f,(id (dom g))] = [(cod f),(dom g)] by Th22;

cod (id (dom f)) = dom f ;

then A4: cod [(id (dom f)),g] = [(dom f),(cod g)] by Th22;

dom (id (cod g)) = cod g ;

then A5: dom [f,(id (cod g))] = [(dom f),(cod g)] by Th22;

thus ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((S ?- (cod f)) . g) (*) ((L . (dom g)) . f) by A1

.= ((S ?- (cod f)) . g) (*) ((S -? (dom g)) . f) by A1

.= (S . ((id (cod f)),g)) (*) ((S -? (dom g)) . f) by FUNCT_5:69

.= (S . ((id (cod f)),g)) (*) (S . (f,(id (dom g)))) by FUNCT_5:70

.= S . ([(id (cod f)),g] (*) [f,(id (dom g))]) by A2, A3, CAT_1:64

.= S . [((id (cod f)) (*) f),(g (*) (id (dom g)))] by A2, A3, Th24

.= S . [f,(g (*) (id (dom g)))] by CAT_1:21

.= S . [f,g] by CAT_1:22

.= S . [(f (*) (id (dom f))),g] by CAT_1:22

.= S . [(f (*) (id (dom f))),((id (cod g)) (*) g)] by CAT_1:21

.= S . ([f,(id (cod g))] (*) [(id (dom f)),g]) by A5, A4, Th24

.= (S . (f,(id (cod g)))) (*) (S . [(id (dom f)),g]) by A5, A4, CAT_1:64

.= ((S -? (cod g)) . f) (*) (S . ((id (dom f)),g)) by FUNCT_5:70

.= ((S -? (cod g)) . f) (*) ((S ?- (dom f)) . g) by FUNCT_5:69

.= ((L . (cod g)) . f) (*) ((S ?- (dom f)) . g) by A1

.= ((L . (cod g)) . f) (*) ((M . (dom f)) . g) by A1 ; :: thesis: verum