theorem LemmaA: :: LOPBAN12:1

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