let C, D be non empty category; :: thesis: for F being covariant Functor of C,D holds F is Functor of Alter C, Alter D
let F be covariant Functor of C,D; :: thesis: F is Functor of Alter C, Alter D
reconsider F1 = F as Function of the carrier' of (Alter C), the carrier' of (Alter D) ;
A1: ( F is identity-preserving & F is multiplicative ) by Def25;
A2: for a being Object of (Alter C) ex b being Object of (Alter D) st F1 . (id a) = id b

proof

let a be Object of (Alter C); :: thesis: ex b being Object of (Alter D) st F1 . (id a) = id b
reconsider a1 = id a as morphism of C ;
a1 is identity by Th47;
then consider b being Object of (Alter D) such that
A3: F . a1 = id b by Th47, A1;
take b ; :: thesis: F1 . (id a) = id b
thus F1 . (id a) = id b by A3, Def21; :: thesis: verum

end;

A4: for f being Morphism of (Alter C) holds
( F1 . (id (dom f)) = id (dom (F1 . f)) & F1 . (id (cod f)) = id (cod (F1 . f)) )

proof

let f be Morphism of (Alter C); :: thesis: ( F1 . (id (dom f)) = id (dom (F1 . f)) & F1 . (id (cod f)) = id (cod (F1 . f)) )
reconsider o1 = dom f as Object of (Alter C) ;
reconsider o2 = o1 as Object of C ;
reconsider f1 = f as morphism of C ;
A5: F . f1 = F1 . f by Def21;
A6: F . o2 = F1 . (dom f1) by Th45
.= dom (F . f1) by Th32
.= dom (F1 . f) by Th45, A5 ;
thus F1 . (id (dom f)) = F1 . (id- o2) by Th46
.= id- (F . o2)
.= id (dom (F1 . f)) by A6, Th46 ; :: thesis: F1 . (id (cod f)) = id (cod (F1 . f))
reconsider o3 = cod f as Object of (Alter C) ;
reconsider o4 = o3 as Object of C ;
reconsider f1 = f as morphism of C ;
A7: F . f1 = F1 . f by Def21;
A8: F . o3 = F1 . (cod f1) by Th45
.= cod (F . f1) by Th32
.= cod (F1 . f) by Th45, A7 ;
thus F1 . (id (cod f)) = F1 . (id- o4) by Th46
.= id- (F . o4)
.= id (cod (F1 . f)) by A8, Th46 ; :: thesis: verum

end;

for f, g being Morphism of (Alter C) st dom g = cod f holds
F1 . (g (*) f) = (F1 . g) (*) (F1 . f)

proof

let f, g be Morphism of (Alter C); :: thesis: ( dom g = cod f implies F1 . (g (*) f) = (F1 . g) (*) (F1 . f) )
assume A9: dom g = cod f ; :: thesis: F1 . (g (*) f) = (F1 . g) (*) (F1 . f)
reconsider f1 = f, g1 = g as morphism of C ;
A10: [g1,f1] in dom the composition of C by A9, CAT_1:15;
A11: g1 |> f1 by A9, CAT_1:15;
A12: the composition of C . (g1,f1) = g1 (*) f1 by A10, Def2, Def3;
A13: ( F . g1 = F1 . g & F . f1 = F1 . f ) by Def21;
A14: [(F1 . g),(F1 . f)] in dom the Comp of (Alter D) by A13, Def2, A11, A1;
thus F1 . (g (*) f) = F1 . ( the Comp of (Alter C) . (g,f)) by A9, CAT_1:16
.= F . (g1 (*) f1) by A12, Def21
.= (F . g1) (*) (F . f1) by A11, A1
.= the Comp of (Alter D) . ((F1 . g),(F1 . f)) by A13, Def3, A11, A1
.= (F1 . g) (*) (F1 . f) by A14, CAT_1:def 1 ; :: thesis: verum

end;

hence F is Functor of Alter C, Alter D by A2, A4, CAT_1:61; :: thesis: verum