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