let C, D, E be with_identities CategoryStr ; :: thesis: for F being Functor of C,D
for G being Functor of D,E
for f being morphism of C st F is covariant & G is covariant & not C is empty holds
(G (*) F) . f = G . (F . f)
let F be Functor of C,D; :: thesis: for G being Functor of D,E
for f being morphism of C st F is covariant & G is covariant & not C is empty holds
(G (*) F) . f = G . (F . f)
let G be Functor of D,E; :: thesis: for f being morphism of C st F is covariant & G is covariant & not C is empty holds
(G (*) F) . f = G . (F . f)
let f be morphism of C; :: thesis: ( F is covariant & G is covariant & not C is empty implies (G (*) F) . f = G . (F . f) )
assume A1: F is covariant ; :: thesis: ( not G is covariant or C is empty or (G (*) F) . f = G . (F . f) )
assume A2: G is covariant ; :: thesis: ( C is empty or (G (*) F) . f = G . (F . f) )
assume A3: not C is empty ; :: thesis: (G (*) F) . f = G . (F . f)
then A4: not D is empty by A1, Th29;
then A5: not E is empty by A2, Th29;
reconsider x = f as object ;
A6: dom (G (*) F) = the carrier of C by A5, FUNCT_2:def 1;
A7: F . x = F . f by A3, Def21;
then A8: G . (F . x) = G . (F . f) by A4, Def21;
A9: dom F = the carrier of C by A4, FUNCT_2:def 1;
dom G = the carrier of D by A5, FUNCT_2:def 1;
then ( [x,(F . x)] in F & [(F . x),(G . (F . x))] in G ) by A3, A4, A9, A7, FUNCT_1:1;
then [f,(G . (F . f))] in F * G by A8, RELAT_1:def 8;
then A10: [f,(G . (F . f))] in G (*) F by A1, A2, Def27;
thus (G (*) F) . f = (G (*) F) . x by A3, Def21
.= G . (F . f) by A10, A6, FUNCT_1:def 2 ; :: thesis: verum