let C be category; :: thesis: ( C is empty implies C is initial )
assume A1: C is empty ; :: thesis: C is initial
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; :: thesis: 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 Functor of C,C1;
take the Functor of C,C1 ; :: thesis: ( the Functor of C,C1 is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
the Functor of C,C1 = F1 ) )
thus the Functor of C,C1 is covariant by A1; :: thesis: for F1 being Functor of C,C1 st F1 is covariant holds
the Functor of C,C1 = F1
let F1 be Functor of C,C1; :: thesis: ( F1 is covariant implies the Functor of C,C1 = F1 )
assume F1 is covariant ; :: thesis: the Functor of C,C1 = F1
thus the Functor of C,C1 = F1 by A1; :: thesis: verum

end;

hence C is initial ; :: thesis: verum