theorem :: PARTFUN1:78

for A being set st A is functional & ( for f, g being Function st f in A & g in A holds
f tolerates g ) holds
union A is Function