let C1 be empty category; :: thesis: for C2 being category
for E being Functor of ((OrdC 1) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 1,E is_exponent_of C1,C2
let C2 be category; :: thesis: for E being Functor of ((OrdC 1) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 1,E is_exponent_of C1,C2
let E be Functor of ((OrdC 1) [x] C1),C2; :: thesis: ( E = OrdC0-> C2 implies OrdC 1,E is_exponent_of C1,C2 )
assume E = OrdC0-> C2 ; :: thesis: OrdC 1,E is_exponent_of C1,C2
set C = OrdC 1;
reconsider E = E as Functor of ((OrdC 1) [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 1) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 1) 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 1) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 1) 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 1) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 1) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) ) )
assume F is covariant ; :: thesis: ex H being Functor of D,(OrdC 1) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 1) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
set H = D ->OrdC1 ;
reconsider H = D ->OrdC1 as Functor of D,(OrdC 1) ;
take H ; :: thesis: ( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 1) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
thus H is covariant ; :: thesis: ( F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 1) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
thus F = E (*) (H [x] (id C1)) ; :: thesis: for H1 being Functor of D,(OrdC 1) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1
let H1 be Functor of D,(OrdC 1); :: thesis: ( H1 is covariant & F = E (*) (H1 [x] (id C1)) implies H = H1 )
assume A1: H1 is covariant ; :: thesis: ( not F = E (*) (H1 [x] (id C1)) or H = H1 )
consider H2 being Functor of D,(OrdC 1) such that
A2: ( H2 is covariant & ( for H3 being Functor of D,(OrdC 1) st H3 is covariant holds
H2 = H3 ) ) by Def4;
assume F = E (*) (H1 [x] (id C1)) ; :: thesis: H = H1
thus H = H2 by A2
.= H1 by A2, A1 ; :: thesis: verum

end;

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