let C, D, E be with_identities CategoryStr ; :: thesis: for F being Functor of C,D
for G being Functor of D,E st F is covariant & G is covariant holds
G (*) F is covariant
let F be Functor of C,D; :: thesis: for G being Functor of D,E st F is covariant & G is covariant holds
G (*) F is covariant
let G be Functor of D,E; :: thesis: ( F is covariant & G is covariant implies G (*) F is covariant )
assume A1: F is covariant ; :: thesis: ( not G is covariant or G (*) F is covariant )
assume A2: G is covariant ; :: thesis: G (*) F is covariant
set GF = G (*) F;
for f being morphism of C st f is identity holds
(G (*) F) . f is identity

proof

let f be morphism of C; :: thesis: ( f is identity implies (G (*) F) . f is identity )
assume A3: f is identity ; :: thesis: (G (*) F) . f is identity

per cases ( not C is empty or C is empty ) ;

suppose A4: not C is empty ; :: thesis: (G (*) F) . f is identity

A7: F . f is identity by A1, A3, Def22;
(G (*) F) . f = G . (F . f) by A1, A2, Th34, A4;
hence (G (*) F) . f is identity by A2, A7, Def22; :: thesis: verum

end;

suppose A8: C is empty ; :: thesis: (G (*) F) . f is identity

per cases ( not E is empty or E is empty ) ;

suppose A9: not E is empty ; :: thesis: (G (*) F) . f is identity

(G (*) F) . f = the Object of E by A8, Def21;
hence (G (*) F) . f is identity by A9, Th22; :: thesis: verum

end;

suppose E is empty ; :: thesis: (G (*) F) . f is identity

hence (G (*) F) . f is identity by Th10; :: thesis: verum

end;

end;

end;

end;

end;

then A10: G (*) F is identity-preserving ;
for f1, f2 being morphism of C st f1 |> f2 holds
( (G (*) F) . f1 |> (G (*) F) . f2 & (G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2) )

proof

let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( (G (*) F) . f1 |> (G (*) F) . f2 & (G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2) ) )
assume A11: f1 |> f2 ; :: thesis: ( (G (*) F) . f1 |> (G (*) F) . f2 & (G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2) )
then A12: not C is empty ;
A15: (G (*) F) . f1 = G . (F . f1) by A12, A1, A2, Th34;
A16: G is multiplicative by A2;
F is multiplicative by A1;
then A17: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) by A11;
then ( G . (F . f1) |> G . (F . f2) & G . ((F . f1) (*) (F . f2)) = (G . (F . f1)) (*) (G . (F . f2)) ) by A16;
hence (G (*) F) . f1 |> (G (*) F) . f2 by A15, A12, A1, A2, Th34; :: thesis: (G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2)
thus (G (*) F) . (f1 (*) f2) = G . (F . (f1 (*) f2)) by A12, A1, A2, Th34
.= (G . (F . f1)) (*) (G . (F . f2)) by A17, A16
.= ((G (*) F) . f1) (*) ((G (*) F) . f2) by A15, A12, A1, A2, Th34 ; :: thesis: verum

end;

hence G (*) F is covariant by A10, Def23; :: thesis: verum