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;
( f in Funct a,b & Funct a,b in { (Funct a,b) where a, b is Element of AA : verum } ) by CAT_2:def 2;
then reconsider FF = union { (Funct a,b) where a, b is Element of AA : verum } as non empty set by TARSKI:def 4;

A1: 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 ( F in FF & G in FF ) ; :: thesis: G * F in FF
( G * F in Funct A,C & Funct A,C in { (Funct a,b) where a, b is Element of AA : verum } ) by CAT_2:def 2;
hence G * F in FF by TARSKI:def 4; :: thesis: verum

end;

now

let A be Element of AA; :: thesis: id A in FF
( id A in Funct A,A & Funct A,A in { (Funct a,b) where a, b is Element of AA : verum } ) by CAT_2:def 2;
hence id A in FF by TARSKI:def 4; :: thesis: verum

end;

then consider C being strict Categorial Category such that
A2: ( the carrier of C = AA & ( 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 A1, 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 ( a is Object of C & b is Object of C ) ; :: thesis: for F being Functor of a,b holds [[a,b],F] is Morphism of C
then reconsider A = a, B = b as Element of AA by A2;
let F be Functor of a,b; :: thesis: [[a,b],F] is Morphism of C
( F in Funct A,B & Funct A,B in { (Funct a,b) where a, b is Element of AA : verum } ) by CAT_2:def 2;
then F in FF by TARSKI:def 4;
then [[A,B],F] is Morphism of C by A2;
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 A2; :: thesis: verum