theorem Th14: :: MSSUBFAM:14

for I being set
for i being object
for F being ManySortedFunction of I
for f being Function st i in I & f = F . i holds
(doms F) . i = dom f