thus ex F being covariant Functor of C,(OrdC 1) st verum ; :: thesis: for b₁, b₂ being covariant Functor of C,(OrdC 1) holds b₁ = b₂
let F1, F2 be covariant Functor of C,(OrdC 1); :: thesis: F1 = F2
consider F being Functor of C,(OrdC 1) such that
A1: ( F is covariant & ( for F1 being Functor of C,(OrdC 1) st F1 is covariant holds
F = F1 ) ) by Def4;
thus F1 = F by A1
.= F2 by A1 ; :: thesis: verum