let C, B, 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 by CAT_1:44;
then A2: dom [(id (cod f)),g] = [(cod f),(dom g)] by Th38;
cod (id (dom g)) = dom g by CAT_1:44;
then A3: cod [f,(id (dom g))] = [(cod f),(dom g)] by Th38;
cod (id (dom f)) = dom f by CAT_1:44;
then A4: cod [(id (dom f)),g] = [(dom f),(cod g)] by Th38;
dom (id (cod g)) = cod g by CAT_1:44;
then A5: dom [f,(id (cod g))] = [(dom f),(cod g)] by Th38;
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 Th3
.= (S . ((id (cod f)),g)) * (S . (f,(id (dom g)))) by Th4
.= S . ([(id (cod f)),g] * [f,(id (dom g))]) by A2, A3, CAT_1:99
.= S . [((id (cod f)) * f),(g * (id (dom g)))] by A2, A3, Th40
.= S . [f,(g * (id (dom g)))] by CAT_1:46
.= S . [f,g] by CAT_1:47
.= S . [(f * (id (dom f))),g] by CAT_1:47
.= S . [(f * (id (dom f))),((id (cod g)) * g)] by CAT_1:46
.= S . ([f,(id (cod g))] * [(id (dom f)),g]) by A5, A4, Th40
.= (S . (f,(id (cod g)))) * (S . [(id (dom f)),g]) by A5, A4, CAT_1:99
.= ((S -? (cod g)) . f) * (S . ((id (dom f)),g)) by Th4
.= ((S -? (cod g)) . f) * ((S ?- (dom f)) . g) by Th3
.= ((L . (cod g)) . f) * ((S ?- (dom f)) . g) by A1
.= ((L . (cod g)) . f) * ((M . (dom f)) . g) by A1 ; :: thesis: verum