for n being Element of NAT
for D, E being non empty set
for F being Function of D,(HFuncs E) st rng F is compatible & ( for x being Element of D holds dom (F . x) c= n -tuples_on E ) holds
ex f being Element of HFuncs E st
( f = Union F & dom f c= n -tuples_on E )