let C, D be non empty composable with_identities CategoryStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum