let C, D be non empty composable with_identities CategoryStr ; for F being covariant Functor of C,D
for f being morphism of C holds
( F . (dom f) = dom (F . f) & F . (cod f) = cod (F . f) )
let F be covariant Functor of C,D; for f being morphism of C holds
( F . (dom f) = dom (F . f) & F . (cod f) = cod (F . f) )
let f be morphism of C; ( F . (dom f) = dom (F . f) & F . (cod f) = cod (F . f) )
A1:
F is multiplicative
by Def25;
consider d being morphism of C such that
A2:
( dom f = d & f |> d & d is identity )
by Def18;
F . (dom f) in Ob D
;
then reconsider d1 = F . (dom f) as morphism of D ;
A3:
F . f |> F . d
by A2, A1;
A4:
F . d = F . (dom f)
by A2, Def21;
d1 is identity
by Th22;
hence
F . (dom f) = dom (F . f)
by A3, A4, Def18; F . (cod f) = cod (F . f)
consider c being morphism of C such that
A5:
( cod f = c & c |> f & c is identity )
by Def19;
F . (cod f) in Ob D
;
then reconsider c1 = F . (cod f) as morphism of D ;
A6:
F . c |> F . f
by A5, A1;
A7:
F . c = F . (cod f)
by A5, Def21;
c1 is identity
by Th22;
hence
F . (cod f) = cod (F . f)
by A6, A7, Def19; verum