set A = 1Cat 0 ,1;
reconsider C = 1Cat (1Cat 0 ,1),[[(1Cat 0 ,1),(1Cat 0 ,1)],(id (1Cat 0 ,1))] 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 ,1 by A1, TARSKI:def 1;
A4: b = 1Cat 0 ,1 by A2, TARSKI:def 1;
then id (1Cat 0 ,1) = F by A3, FUNCT_2:66;
hence [[a,b],F] is Morphism of C by A3, A4, TARSKI:def 1; :: thesis: verum