let n be Element of NAT ; :: thesis:
let D, E be non empty set ; :: thesis:
set X = D;
set Y = E;
let F be Function of D,(HFuncs E); :: thesis:
assume A1: rng F is compatible ; :: thesis:
assume A2: for x being Element of D holds dom (F . x) c= n -tuples_on E ; :: thesis:
A3: rng F is functional

end;

then reconsider rngF = rng F as non empty functional compatible set by A1;
set D = { (dom g) where g is Element of rngF : verum } ;
reconsider f = Union F as Function by A1, A3;
A5: rng f c= E

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A6: x in dom f and
A7: f . x = y by FUNCT_1:def 3;
x in union { (dom g) where g is Element of rngF : verum } by A6, Th11;
then consider d being set such that
A8: x in d and
A9: d in { (dom g) where g is Element of rngF : verum } by TARSKI:def 4;
consider g being Element of rngF such that
A10: d = dom g by A9;
rng F c= HFuncs E by RELAT_1:def 19;
then reconsider g = g as Element of HFuncs E ;
A11: g . x in rng g by A8, A10, FUNCT_1:3;
A12: rng g c= E by RELAT_1:def 19;
f . x = g . x by A8, A10, Th12;
hence y in E by A7, A12, A11; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dom f ; :: thesis:
then x in union { (dom g) where g is Element of rngF : verum } by Th11;
then consider d being set such that
A14: x in d and
A15: d in { (dom g) where g is Element of rngF : verum } by TARSKI:def 4;
consider g being Element of rngF such that
A16: d = dom g by A15;
consider e being object such that
A17: e in dom F and
A18: F . e = g by FUNCT_1:def 3;
reconsider e = e as Element of D by A17;
dom (F . e) c= n -tuples_on E by A2;
hence x in n -tuples_on E by A14, A16, A18; :: thesis:

end;

n -tuples_on E c= E * by FINSEQ_2:142;
then dom f c= E * by A13;
then reconsider f = f as PartFunc of (E *),E by A5, RELSET_1:4;
reconsider f = f as Element of PFuncs ((E *),E) by PARTFUN1:45;
f is homogeneous by A13;
then f in { g where g is Element of PFuncs ((E *),E) : g is homogeneous } ;
then reconsider f = Union F as Element of HFuncs E ;
take f ; :: thesis:
thus f = Union F ; :: thesis:
thus dom f c= n -tuples_on E by A13; :: thesis: