:: deftheorem Def13 defines Carrier PRALG_1:def 14 :
for A being 1-sorted-yielding Function
for b₂ being Function holds
( b₂ = Carrier A iff ( dom b₂ = dom A & ( for j being set st j in dom A holds
ex R being 1-sorted st
( R = A . j & b₂ . j = the carrier of R ) ) ) );