theorem :: LOPBAN10:33

for X being RealNormSpace-Sequence
for s being Element of (product X) ex F being FinSequence of REAL st
( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(s . i).|| ) )