theorem :: INDEX_1:3

for X being set
for C being Category holds
( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )