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