theorem Th6: :: REAL_NS1:6

for n being Nat
for f being FinSequence of REAL st dom f = Seg n holds
f is Element of REAL n