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 & cod (id (dom g)) = dom g ) by CAT_1:44;
then A2: ( dom [(id (cod f)),g] = [(cod f),(dom g)] & cod [f,(id (dom g))] = [(cod f),(dom g)] ) by Th38;
( dom (id (cod g)) = cod g & cod (id (dom f)) = dom f ) by CAT_1:44;
then A3: ( dom [f,(id (cod g))] = [(dom f),(cod g)] & cod [(id (dom f)),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, CAT_1:99
.= S . [((id (cod f)) * f),(g * (id (dom g)))] by A2, 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 A3, Th40
.= (S . f,(id (cod g))) * (S . [(id (dom f)),g]) by A3, 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