for S being 1-sorted
for M being set holds Carrier (M --> S) = M --> the carrier of S