theorem Th8: :: LOPBAN_7:8

for X, Y being RealNormSpace
for seqx being sequence of X
for seqy being sequence of Y
for x being Point of X
for y being Point of Y holds
( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y iff ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] ) )