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 } ;
consider a, b being Element of AA, f being Functor of a,b;
A1: 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 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

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

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