set A = 1Cat (0,{0});
reconsider C = 1Cat ((1Cat (0,{0})),[[(1Cat (0,{0})),(1Cat (0,{0}))],(id (1Cat (0,{0})))]) as strict Categorial Category by Th11;
take C ; :: thesis: C is full
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
A1: a is Object of C and
A2: b is Object of C ; :: thesis: for F being Functor of a,b holds [[a,b],F] is Morphism of C
let F be Functor of a,b; :: thesis: [[a,b],F] is Morphism of C
A3: a = 1Cat (0,{0}) by A1, TARSKI:def 1;
A4: b = 1Cat (0,{0}) by A2, TARSKI:def 1;
then id (1Cat (0,{0})) = F by A3, FUNCT_2:51;
hence [[a,b],F] is Morphism of C by A3, A4, TARSKI:def 1; :: thesis: verum