per cases ( C1 is empty or ( C2 is empty & not C1 is empty ) or ( not C1 is empty & not C2 is empty ) ) ;

suppose A1: C1 is empty ; :: thesis: ex b₁ being pair object ex C being category ex E being Functor of (C [x] C1),C2 st
( b₁ = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )

set C = OrdC 1;
reconsider E = OrdC0-> C2 as Functor of ((OrdC 1) [x] C1),C2 by A1;
set IT = [(OrdC 1),E];
take [(OrdC 1),E] ; :: thesis: ex C being category ex E being Functor of (C [x] C1),C2 st
( [(OrdC 1),E] = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )
take OrdC 1 ; :: thesis: ex E being Functor of ((OrdC 1) [x] C1),C2 st
( [(OrdC 1),E] = [(OrdC 1),E] & E is covariant & OrdC 1,E is_exponent_of C1,C2 )
take E ; :: thesis: ( [(OrdC 1),E] = [(OrdC 1),E] & E is covariant & OrdC 1,E is_exponent_of C1,C2 )
thus ( [(OrdC 1),E] = [(OrdC 1),E] & E is covariant & OrdC 1,E is_exponent_of C1,C2 ) by A1, Lm8; :: thesis: verum

end;

suppose A2: ( C2 is empty & not C1 is empty ) ; :: thesis: ex b₁ being pair object ex C being category ex E being Functor of (C [x] C1),C2 st
( b₁ = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )

set C = OrdC 0;
reconsider E = OrdC0-> C2 as Functor of ((OrdC 0) [x] C1),C2 ;
set IT = [(OrdC 0),E];
take [(OrdC 0),E] ; :: thesis: ex C being category ex E being Functor of (C [x] C1),C2 st
( [(OrdC 0),E] = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )
take OrdC 0 ; :: thesis: ex E being Functor of ((OrdC 0) [x] C1),C2 st
( [(OrdC 0),E] = [(OrdC 0),E] & E is covariant & OrdC 0,E is_exponent_of C1,C2 )
take E ; :: thesis: ( [(OrdC 0),E] = [(OrdC 0),E] & E is covariant & OrdC 0,E is_exponent_of C1,C2 )
thus ( [(OrdC 0),E] = [(OrdC 0),E] & E is covariant & OrdC 0,E is_exponent_of C1,C2 ) by A2, Lm7; :: thesis: verum

end;

suppose A3: ( not C1 is empty & not C2 is empty ) ; :: thesis: ex b₁ being pair object ex C being category ex E being Functor of (C [x] C1),C2 st
( b₁ = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )

set C = Functors (C1,C2);
consider E being Functor of ((Functors (C1,C2)) [x] C1),C2 such that
A4: E is covariant and
A5: for D being category
for F being Functor of (D [x] C1),C2 st F is covariant holds
ex H being Functor of D,(Functors (C1,C2)) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(Functors (C1,C2)) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) ) by A3, Lm6;
set IT = [(Functors (C1,C2)),E];
take [(Functors (C1,C2)),E] ; :: thesis: ex C being category ex E being Functor of (C [x] C1),C2 st
( [(Functors (C1,C2)),E] = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )
take Functors (C1,C2) ; :: thesis: ex E being Functor of ((Functors (C1,C2)) [x] C1),C2 st
( [(Functors (C1,C2)),E] = [(Functors (C1,C2)),E] & E is covariant & Functors (C1,C2),E is_exponent_of C1,C2 )
take E ; :: thesis: ( [(Functors (C1,C2)),E] = [(Functors (C1,C2)),E] & E is covariant & Functors (C1,C2),E is_exponent_of C1,C2 )
thus ( [(Functors (C1,C2)),E] = [(Functors (C1,C2)),E] & E is covariant & Functors (C1,C2),E is_exponent_of C1,C2 ) by A5, A4, Def34; :: thesis: verum

end;

end;