theorem :: COMPUT_1:40

for D being non empty set
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