Mor (OrdC 0) = {}
;
then reconsider C = OrdC 0 as empty strict category ;
for C1 being category ex F being Functor of C,C1 st
( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
F = F1 ) )
proof
let C1 be
category;
ex F being Functor of C,C1 st
( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
F = F1 ) )
set F = the
covariant Functor of
C,
C1;
take
the
covariant Functor of
C,
C1
;
( the covariant Functor of C,C1 is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
the covariant Functor of C,C1 = F1 ) )
thus
the
covariant Functor of
C,
C1 is
covariant
;
for F1 being Functor of C,C1 st F1 is covariant holds
the covariant Functor of C,C1 = F1
let F1 be
Functor of
C,
C1;
( F1 is covariant implies the covariant Functor of C,C1 = F1 )
assume
F1 is
covariant
;
the covariant Functor of C,C1 = F1
thus
the
covariant Functor of
C,
C1 = F1
;
verum
end;
hence
( OrdC 0 is empty & OrdC 0 is initial )
; verum