let A, B be Category; :: thesis: for F being Functor of A,B holds F is covariant Functor of (alter A),(alter B)
let F be Functor of A,B; :: thesis: F is covariant Functor of (alter A),(alter B)
reconsider F1 = F as Function of (alter A),(alter B) ;
for f1, f2 being morphism of (alter A) st f1 |> f2 holds
( F1 . f1 |> F1 . f2 & F1 . (f1 (*) f2) = (F1 . f1) (*) (F1 . f2) )

proof

let f1, f2 be morphism of (alter A); :: thesis: ( f1 |> f2 implies ( F1 . f1 |> F1 . f2 & F1 . (f1 (*) f2) = (F1 . f1) (*) (F1 . f2) ) )
assume A1: f1 |> f2 ; :: thesis: ( F1 . f1 |> F1 . f2 & F1 . (f1 (*) f2) = (F1 . f1) (*) (F1 . f2) )
reconsider a1 = f1, a2 = f2 as Morphism of A ;
A2: dom a1 = cod a2 by A1, CAT_1:15;
( dom (F . a1) = F . (dom a1) & cod (F . a2) = F . (cod a2) ) by CAT_1:72;
then dom (F . a1) = cod (F . a2) by A1, CAT_1:15;
then A3: [(F . a1),(F . a2)] in dom the Comp of B by CAT_1:15;
A4: F1 . f1 = F . a1 by Def21;
A5: F1 . f2 = F . a2 by Def21;
thus F1 . f1,F1 . f2 are_composable by A3, A4, Def21; :: thesis: F1 . (f1 (*) f2) = (F1 . f1) (*) (F1 . f2)
f1 (*) f2 = a1 (*) a2 by A1, Th41;
hence F1 . (f1 (*) f2) = F . (a1 (*) a2) by Def21
.= (F . a1) (*) (F . a2) by A2, CAT_1:64
.= (F1 . f1) (*) (F1 . f2) by A3, A4, A5, Th41 ;
:: thesis: verum

end;

then A6: F1 is multiplicative ;
for f being morphism of (alter A) st f is identity holds
F1 . f is identity

proof

let f be morphism of (alter A); :: thesis: ( f is identity implies F1 . f is identity )
assume f is identity ; :: thesis: F1 . f is identity
then consider o being Object of A such that
A7: f = id o by Th42;
consider o1 being Object of B such that
A8: F . (id o) = id o1 by CAT_1:62;
thus F1 . f is identity by Def21, A7, A8, Th42; :: thesis: verum

end;

hence F is covariant Functor of (alter A),(alter B) by A6, Def25, Def22; :: thesis: verum