let AA be non empty categorial set ; ex C being strict Categorial full Category st the carrier of C = AA
set dFF = { (Funct (a,b)) where a, b is Element of AA : verum } ;
set a = the Element of AA;
set f = the Functor of the Element of AA, the Element of AA;
A1:
the Functor of the Element of AA, the Element of AA in Funct ( the Element of AA, the Element of AA)
by CAT_2:def 2;
Funct ( the Element of AA, the Element of AA) in { (Funct (a,b)) where a, b is Element of AA : verum }
;
then reconsider FF = union { (Funct (a,b)) where a, b is Element of AA : verum } as non empty set by A1, TARSKI:def 4;
A2:
now for A, B, C being Element of AA
for F being Functor of A,B
for G being Functor of B,C st F in FF & G in FF holds
G * F in FFlet A,
B,
C be
Element of
AA;
for F being Functor of A,B
for G being Functor of B,C st F in FF & G in FF holds
G * F in FFlet F be
Functor of
A,
B;
for G being Functor of B,C st F in FF & G in FF holds
G * F in FFlet G be
Functor of
B,
C;
( F in FF & G in FF implies G * F in FF )assume that
F in FF
and
G in FF
;
G * F in FFA3:
G * F in Funct (
A,
C)
by CAT_2:def 2;
Funct (
A,
C)
in { (Funct (a,b)) where a, b is Element of AA : verum }
;
hence
G * F in FF
by A3, TARSKI:def 4;
verum end;
then consider C being strict Categorial Category such that
A5:
the carrier of C = AA
and
A6:
for A, B being Element of AA
for F being Functor of A,B holds
( [[A,B],F] is Morphism of C iff F in FF )
by A2, Th17;
C is full
proof
let a,
b be
Category;
CAT_5:def 8 ( a is Object of C & b is Object of C implies for F being Functor of a,b holds [[a,b],F] is Morphism of C )
assume that A7:
a is
Object of
C
and A8:
b is
Object of
C
;
for F being Functor of a,b holds [[a,b],F] is Morphism of C
reconsider A =
a,
B =
b as
Element of
AA by A5, A7, A8;
let F be
Functor of
a,
b;
[[a,b],F] is Morphism of C
A9:
F in Funct (
A,
B)
by CAT_2:def 2;
Funct (
A,
B)
in { (Funct (a,b)) where a, b is Element of AA : verum }
;
then
F in FF
by A9, TARSKI:def 4;
then
[[A,B],F] is
Morphism of
C
by A6;
hence
[[a,b],F] is
Morphism of
C
;
verum
end;
hence
ex C being strict Categorial full Category st the carrier of C = AA
by A5; verum