theorem :: ISOCAT_1:16

for A being Category
for o, m being set holds [:(1Cat (o,m)),A:] ~= A