let n be 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 )
A3: rng F is functional

proof

let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in rng F or x is set )
A4: rng F c= HFuncs E by RELAT_1:def 19;
assume x in rng F ; :: thesis: x is set
hence x is set by A4; :: 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, A3;
A5: rng f c= E

proof

let y be object ; :: 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 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: verum

end;

A13: dom f c= n -tuples_on E

proof

let x be object ; :: 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 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: verum

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: ( 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 A13; :: thesis: verum