let C1, C2 be with_identities CategoryStr ; :: thesis: for f1, f2 being morphism of C1
for F being Functor of C1,C2 st F is covariant & f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
let f1, f2 be morphism of C1; :: thesis: for F being Functor of C1,C2 st F is covariant & f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
let F be Functor of C1,C2; :: thesis: ( F is covariant & f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
assume F is covariant ; :: thesis: ( not f1 |> f2 or ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
then A1: F is multiplicative by CAT_6:def 25;
assume f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
hence ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) by A1, CAT_6:def 23; :: thesis: verum