theorem Th15: :: PRALG_1:16

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