theorem Th45: :: NDIFF_5:45

for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (product G),S
for x, y being Point of (product G) ex h being FinSequence of (product G) ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Point of (product G) st i in dom h & h /. i = hi holds
||.hi.|| <= ||.y.|| ) & (f /. (x + y)) - (f /. x) = Sum g )