theorem Th15: :: NDIFF14:15

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for k being Element of dom S
for f being PartFunc of (product S),T holds f `partial| (Z,<*k*>) = f `partial| (Z,k)