let D be non empty set ; :: thesis: for F being Function of NAT ,(HFuncs D) st ( for i being Element of NAT holds F . i c= F . (i + 1) ) holds
Union F in HFuncs D
set X = D;
let F be Function of NAT ,(HFuncs D); :: thesis: ( ( for i being Element of NAT holds F . i c= F . (i + 1) ) implies Union F in HFuncs D )
assume A1: for i being Element of NAT holds F . i c= F . (i + 1) ; :: thesis: Union F in HFuncs D

A2: now

let n be Element of NAT ; :: thesis: for m being Element of NAT st n <= m holds
F . n c= F . m
defpred S₁[ Element of NAT ] means F . n c= F . (n + $1);
let m be Element of NAT ; :: thesis: ( n <= m implies F . n c= F . m )

A3: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
F . (n + i) c= F . ((n + i) + 1) by A1;
hence S₁[i + 1] by A4, XBOOLE_1:1; :: thesis: verum

end;

A5: S₁[ 0 ] ;
A6: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A5, A3);
assume n <= m ; :: thesis: F . n c= F . m
then consider i being Nat such that
A7: m = n + i by NAT_1:10;
i in NAT by ORDINAL1:def 13;
hence F . n c= F . m by A6, A7; :: thesis: verum

end;

reconsider Y = rng F as non empty Subset of (HFuncs D) by RELAT_1:def 19;
A8: Y is compatible

proof

let f, g be Function; :: according to COMPUT_1:def 1 :: thesis: ( f in Y & g in Y implies f tolerates g )
assume f in Y ; :: thesis: ( not g in Y or f tolerates g )
then consider i being set such that
A9: i in dom F and
A10: f = F . i by FUNCT_1:def 5;
assume g in Y ; :: thesis: f tolerates g
then consider j being set such that
A11: j in dom F and
A12: g = F . j by FUNCT_1:def 5;
reconsider i = i, j = j as Element of NAT by A9, A11;
( i <= j or j <= i ) ;
hence f tolerates g by A2, A10, A12, PARTFUN1:135; :: thesis: verum

end;

Y is PartFunc-set of D * ,D

proof

let f be Element of Y; :: according to RFUNCT_3:def 3 :: thesis: f is Element of bool [:(D * ),D:]
f is Element of HFuncs D ;
hence f is Element of bool [:(D * ),D:] ; :: thesis: verum

end;

then Union F is PartFunc of (D * ),D by A8, Th18;
then reconsider f = Union F as Element of PFuncs (D * ),D by PARTFUN1:119;
A14: dom f = union { (dom g) where g is Element of Y : verum } by A8, Th15;
f is homogeneous

proof

thus dom f is with_common_domain :: according to MARGREL1:def 22 :: thesis: verum

proof

let x, y be FinSequence; :: according to MARGREL1:def 1 :: thesis: ( not x in dom f or not y in dom f or len x = len y )
assume x in dom f ; :: thesis: ( not y in dom f or len x = len y )
then consider A1 being set such that
A15: x in A1 and
A16: A1 in { (dom g) where g is Element of Y : verum } by A14, TARSKI:def 4;
consider g1 being Element of Y such that
A17: A1 = dom g1 by A16;
assume y in dom f ; :: thesis: len x = len y
then consider A2 being set such that
A18: y in A2 and
A19: A2 in { (dom g) where g is Element of Y : verum } by A14, TARSKI:def 4;
consider g2 being Element of Y such that
A20: A2 = dom g2 by A19;
consider i1 being set such that
A21: i1 in dom F and
A22: g1 = F . i1 by FUNCT_1:def 5;
consider i2 being set such that
A23: i2 in dom F and
A24: g2 = F . i2 by FUNCT_1:def 5;
reconsider i1 = i1, i2 = i2 as Element of NAT by A21, A23;
( i1 <= i2 or i2 <= i1 ) ;
then ( g1 c= g2 or g2 c= g1 ) by A2, A22, A24;
then ( dom g1 c= dom g2 or dom g2 c= dom g1 ) by GRFUNC_1:8;
then dom x = dom y by A15, A17, A18, A20, CARD_3:def 10;
hence len x = len y by FINSEQ_3:31; :: thesis: verum

end;

end;

hence Union F in HFuncs D ; :: thesis: verum