:: deftheorem Def3 defines Mphs INDEX_1:def 3 :
for F being Category-yielding Function
for b₂ being non-empty Function holds
( b₂ = Mphs 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 ) ) );