theorem Th52: :: REAL_NS2:52

for n being non empty Nat holds RealFuncExtMult (Seg n) = n -Mult_over F_Real