let C, C1, C2 be category; :: thesis: for F1 being Functor of C,C1
for F2 being Functor of C,C2 st F1 is covariant & F2 is covariant holds
(C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2
let F1 be Functor of C,C1; :: thesis: for F2 being Functor of C,C2 st F1 is covariant & F2 is covariant holds
(C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2
let F2 be Functor of C,C2; :: thesis: ( F1 is covariant & F2 is covariant implies (C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2 )
assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: (C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2
consider F being Functor of C,(OrdC 1) such that
A2: ( F is covariant & ( for F1 being Functor of C,(OrdC 1) st F1 is covariant holds
F = F1 ) ) by Def4;
reconsider F11 = (C1 ->OrdC1) (*) F1 as covariant Functor of C,(OrdC 1) by A1, CAT_6:35;
reconsider F22 = (C2 ->OrdC1) (*) F2 as covariant Functor of C,(OrdC 1) by A1, CAT_6:35;
( F11 = F & F22 = F ) by A2;
hence (C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2 ; :: thesis: verum