theorem Th51: :: REAL_NS2:51

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