let C, D be with_identities CategoryStr ; :: thesis: ( not C is empty & D is empty implies for F being Functor of C,D holds
( not F is multiplicative & not F is antimultiplicative ) )
assume A1: not C is empty ; :: thesis: ( not D is empty or for F being Functor of C,D holds
( not F is multiplicative & not F is antimultiplicative ) )
then reconsider f = the Object of C as morphism of C by TARSKI:def 3;
A2: f |> f by A1, Th23;
assume A3: D is empty ; :: thesis: for F being Functor of C,D holds
( not F is multiplicative & not F is antimultiplicative )
assume ex F being Functor of C,D st
( F is multiplicative or F is antimultiplicative ) ; :: thesis: contradiction
then consider F being Functor of C,D such that
A4: ( F is multiplicative or F is antimultiplicative ) ;
A5: not F . f |> F . f by A3;

per cases ( F is multiplicative or F is antimultiplicative ) by A4;

suppose F is multiplicative ; :: thesis: contradiction

hence contradiction by A5, A2; :: thesis: verum

end;

suppose F is antimultiplicative ; :: thesis: contradiction

hence contradiction by A5, A2; :: thesis: verum

end;

end;