theorem :: REAL_NS2:70

for V being RealLinearSpace
for F being set holds
( F is FinSequence of V iff F is FinSequence of (RLSp2RVSp V) ) ;