let n be Element of NAT ; :: thesis: 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 )
let D, E be non empty set ; :: thesis: 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 )
set X = D;
set Y = E;
let F be Function of D,(HFuncs E); :: thesis: ( rng F is compatible & ( for x being Element of D holds dom (F . x) c= n -tuples_on E ) implies ex f being Element of HFuncs E st
( f = Union F & dom f c= n -tuples_on E ) )
assume A1: rng F is compatible ; :: thesis: ( ex x being Element of D st not dom (F . x) c= n -tuples_on E or ex f being Element of HFuncs E st
( f = Union F & dom f c= n -tuples_on E ) )
assume A2: for x being Element of D holds dom (F . x) c= n -tuples_on E ; :: thesis: ex f being Element of HFuncs E st
( f = Union F & dom f c= n -tuples_on E )
A4: rng F is functional

proof

let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in rng F or x is set )
A5: rng F c= HFuncs E by RELAT_1:def 19;
assume x in rng F ; :: thesis: x is set
hence x is set by A5; :: thesis: verum

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, A4;
A7: rng f c= E

proof

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

end;

A16: dom f c= n -tuples_on E

proof

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

end;

n -tuples_on E c= E * by FINSEQ_2:162;
then dom f c= E * by A16, XBOOLE_1:1;
then reconsider f = f as PartFunc of (E * ),E by A7, RELSET_1:11;
reconsider f = f as Element of PFuncs (E * ),E by PARTFUN1:119;
f is homogeneous

proof

thus dom f is with_common_domain by A16; :: according to UNIALG_1:def 1 :: thesis: verum

end;

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: ( f = Union F & dom f c= n -tuples_on E )
thus f = Union F ; :: thesis: dom f c= n -tuples_on E
thus dom f c= n -tuples_on E by A16; :: thesis: verum