A1:
the carrier of (EnsCat {0}) = {0}
by Def14;

hereby :: according to ALTCAT_1:def 19 :: thesis: EnsCat {0} is 1 -element

thus
the carrier of (EnsCat {0}) is 1 -element
by A1; :: according to STRUCT_0:def 19 :: thesis: verumlet i be Object of (EnsCat {0}); :: thesis: <^i,i^> is trivial

i = 0 by A1, TARSKI:def 1;

hence <^i,i^> is trivial by Def14, FUNCT_2:127; :: thesis: verum

end;i = 0 by A1, TARSKI:def 1;

hence <^i,i^> is trivial by Def14, FUNCT_2:127; :: thesis: verum