let AA be non empty categorial set ; :: thesis: 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 :: thesis: 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 FF

let A, B, C be Element of AA; :: thesis: 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 FF
let F be Functor of A,B; :: thesis: for G being Functor of B,C st F in FF & G in FF holds
G * F in FF
let G be Functor of B,C; :: thesis: ( F in FF & G in FF implies G * F in FF )
assume that
F in FF and
G in FF ; :: thesis: G * F in FF
A3: 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; :: thesis: verum

end;

now :: thesis: for A being Element of AA holds id A in FF

let A be Element of AA; :: thesis: id A in FF
A4: id A in Funct (A,A) by CAT_2:def 2;
Funct (A,A) in { (Funct (a,b)) where a, b is Element of AA : verum } ;
hence id A in FF by A4, TARSKI:def 4; :: thesis: 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; :: according to CAT_5:def 8 :: thesis: ( 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 ; :: thesis: 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; :: thesis: [[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 ; :: thesis: verum

end;

hence ex C being strict Categorial full Category st the carrier of C = AA by A5; :: thesis: verum