let C1 be non empty category; :: thesis: for C2 being empty category
for E being Functor of ((OrdC 0) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 0,E is_exponent_of C1,C2
let C2 be empty category; :: thesis: for E being Functor of ((OrdC 0) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 0,E is_exponent_of C1,C2
let E be Functor of ((OrdC 0) [x] C1),C2; :: thesis: ( E = OrdC0-> C2 implies OrdC 0,E is_exponent_of C1,C2 )
assume E = OrdC0-> C2 ; :: thesis: OrdC 0,E is_exponent_of C1,C2
set C = OrdC 0;
reconsider E = E as Functor of ((OrdC 0) [x] C1),C2 ;
for D being category
for F being Functor of (D [x] C1),C2 st F is covariant holds
ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )

proof

let D be category; :: thesis: for F being Functor of (D [x] C1),C2 st F is covariant holds
ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
let F be Functor of (D [x] C1),C2; :: thesis: ( F is covariant implies ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) ) )
assume A1: F is covariant ; :: thesis: ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
set G1 = OrdC0-> (OrdC 0);
A2: D is empty by A1, CAT_6:31;
then reconsider G1 = OrdC0-> (OrdC 0) as Functor of D,(OrdC 0) ;
take G1 ; :: thesis: ( G1 is covariant & F = E (*) (G1 [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
G1 = H1 ) )
thus G1 is covariant by A2; :: thesis: ( F = E (*) (G1 [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
G1 = H1 ) )
thus F = E (*) (G1 [x] (id C1)) ; :: thesis: for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
G1 = H1
thus for G2 being Functor of D,(OrdC 0) st G2 is covariant & F = E (*) (G2 [x] (id C1)) holds
G1 = G2 ; :: thesis: verum

end;

hence OrdC 0,E is_exponent_of C1,C2 by Def34; :: thesis: verum