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