:: deftheorem Def2 defines Objs INDEX_1:def 2 :
for F being Category-yielding Function
for b₂ being non-empty Function holds
( b₂ = Objs F iff ( dom b₂ = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b₂ . x = the carrier of C ) ) );