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

A2: now :: thesis: for n, m being Element of NAT st n <= m holds
F . n c= F . m

let n be Element of NAT ; :: thesis: for m being Element of NAT st n <= m holds
F . n c= F . m
defpred S₁[ 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 :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be 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 Nat holds S₁[i] from NAT_1:sch 2(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;
thus 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 object such that
A9: i in dom F and
A10: f = F . i by FUNCT_1:def 3;
assume g in Y ; :: thesis: f tolerates g
then consider j being object such that
A11: j in dom F and
A12: g = F . j by FUNCT_1:def 3;
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:54; :: 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 K32(K33((D *),D))
f is Element of HFuncs D ;
hence f is Element of K32(K33((D *),D)) ; :: thesis: verum

end;

then Union F is PartFunc of (D *),D by A8, Th14;
then reconsider f = Union F as Element of PFuncs ((D *),D) by PARTFUN1:45;
A13: dom f = union { (dom g) where g is Element of Y : verum } by A8, Th11;
f is homogeneous

proof

thus dom f is with_common_domain :: according to MARGREL1:def 21 :: 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
A14: x in A1 and
A15: A1 in { (dom g) where g is Element of Y : verum } by A13, TARSKI:def 4;
consider g1 being Element of Y such that
A16: A1 = dom g1 by A15;
assume y in dom f ; :: thesis: len x = len y
then consider A2 being set such that
A17: y in A2 and
A18: A2 in { (dom g) where g is Element of Y : verum } by A13, TARSKI:def 4;
consider g2 being Element of Y such that
A19: A2 = dom g2 by A18;
consider i1 being object such that
A20: i1 in dom F and
A21: g1 = F . i1 by FUNCT_1:def 3;
consider i2 being object such that
A22: i2 in dom F and
A23: g2 = F . i2 by FUNCT_1:def 3;
reconsider i1 = i1, i2 = i2 as Element of NAT by A20, A22;
( i1 <= i2 or i2 <= i1 ) ;
then ( g1 c= g2 or g2 c= g1 ) by A2, A21, A23;
then ( dom g1 c= dom g2 or dom g2 c= dom g1 ) by GRFUNC_1:2;
then dom x = dom y by A14, A16, A17, A19, CARD_3:def 10;
hence len x = len y by FINSEQ_3:29; :: thesis: verum

end;

end;

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