let x be object ; :: thesis: for C being CategoryStr st the carrier of C = {x} & the composition of C = {[[x,x],x]} holds
C is non empty category
let C be CategoryStr ; :: thesis: ( the carrier of C = {x} & the composition of C = {[[x,x],x]} implies C is non empty category )
assume A1: the carrier of C = {x} ; :: thesis: ( not the composition of C = {[[x,x],x]} or C is non empty category )
assume A2: the composition of C = {[[x,x],x]} ; :: thesis: C is non empty category
A3: the carrier of C = the carrier of (DiscreteCat {x}) by A1, CAT_6:def 16;
for y being object holds
( y in the composition of (DiscreteCat {x}) iff y in {[[x,x],x]} )

proof

let y be object ; :: thesis: ( y in the composition of (DiscreteCat {x}) iff y in {[[x,x],x]} )

hereby :: thesis: ( y in {[[x,x],x]} implies y in the composition of (DiscreteCat {x}) )

assume y in the composition of (DiscreteCat {x}) ; :: thesis: y in {[[x,x],x]}
then consider x1, x2 being object such that
A4: ( y = [x1,x2] & x1 in [: the carrier of (DiscreteCat {x}), the carrier of (DiscreteCat {x}):] & x2 in the carrier of (DiscreteCat {x}) ) by RELSET_1:2;
A5: ( x1 in [:{x},{x}:] & x2 = x ) by A3, A4, A1, TARSKI:def 1;
x1 in {[x,x]} by ZFMISC_1:29, A3, A4, A1;
then x1 = [x,x] by TARSKI:def 1;
hence y in {[[x,x],x]} by A5, A4, TARSKI:def 1; :: thesis: verum

end;

assume A6: y in {[[x,x],x]} ; :: thesis: y in the composition of (DiscreteCat {x})
x in the carrier of (DiscreteCat {x}) by A3, A1, TARSKI:def 1;
then reconsider f = x as morphism of (DiscreteCat {x}) by CAT_6:def 1;
A7: y = [[f,f],f] by A6, TARSKI:def 1;
A8: not DiscreteCat {x} is empty by CAT_6:def 16;
A9: f is identity by CAT_6:def 15;
A10: f |> f by A8, CAT_6:24, CAT_6:def 15;
then A11: [f,f] in dom the composition of (DiscreteCat {x}) by CAT_6:def 2;
f = f (*) f by A9, A10, Th4;
then the composition of (DiscreteCat {x}) . (f,f) = f by A10, CAT_6:def 3;
then the composition of (DiscreteCat {x}) . [f,f] = f by BINOP_1:def 1;
hence y in the composition of (DiscreteCat {x}) by A7, A11, FUNCT_1:1; :: thesis: verum

end;

then the composition of (DiscreteCat {x}) = {[[x,x],x]} by TARSKI:2;
hence C is non empty category by A3, A2, CAT_6:14, CAT_6:15, CAT_6:20; :: thesis: verum