for n being non empty Nat holds RealFuncAdd (Seg n) = product ( the addF of F_Real,n)