theorem LemmaA: :: LOPBAN12:11

for E, F being RealNormSpace
for s being Point of (product <*E,F*>)
for i being Element of dom <*E,F*>
for x1 being object holds len (s +* (i,x1)) = 2