theorem :: ISOCAT_2:9

for A being Category
for o, m being set holds Functors ((1Cat (o,m)),A) ~= A