theorem Th54: :: NDIFF_5:54

for G being RealNormSpace-Sequence
for h being FinSequence of (product G)
for y, x being Point of (product G)
for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))