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: Union F = union (rng F) by CARD_3:def 4;
reconsider Y = rng F as non empty Subset of (HFuncs D) by RELAT_1:def 19;
A3: 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;

A4: 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);
A5: S₁[ 0 ] ;

A6: now

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

end;

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

end;

A10: 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
A11: ( i in dom F & f = F . i ) by FUNCT_1:def 5;
assume g in Y ; :: thesis: f tolerates g
then consider j being set such that
A12: ( j in dom F & g = F . j ) by FUNCT_1:def 5;
reconsider i = i, j = j as Element of NAT by A11, A12;
( i <= j or j <= i ) ;
hence f tolerates g by A4, A11, A12, PARTFUN1:135; :: thesis: verum

end;

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

proof

let x, y be FinSequence; :: according to UNIALG_1: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
A14: ( x in A1 & A1 in { (dom g) where g is Element of Y : verum } ) by A13, TARSKI:def 4;
consider g1 being Element of Y such that
A15: A1 = dom g1 by A14;
assume y in dom f ; :: thesis: len x = len y
then consider A2 being set such that
A16: ( y in A2 & A2 in { (dom g) where g is Element of Y : verum } ) by A13, TARSKI:def 4;
consider g2 being Element of Y such that
A17: A2 = dom g2 by A16;
consider i1 being set such that
A18: ( i1 in dom F & g1 = F . i1 ) by FUNCT_1:def 5;
consider i2 being set such that
A19: ( i2 in dom F & g2 = F . i2 ) by FUNCT_1:def 5;
reconsider i1 = i1, i2 = i2 as Element of NAT by A18, A19;
( i1 <= i2 or i2 <= i1 ) ;
then ( g1 c= g2 or g2 c= g1 ) by A4, A18, A19;
then ( dom g1 c= dom g2 or dom g2 c= dom g1 ) by GRFUNC_1:8;
hence len x = len y by A14, A15, A16, A17, UNIALG_1:def 1; :: thesis: verum

end;

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