theorem Th16: :: TOPREAL7:16

for n being Element of NAT
for f being FinSequence of REAL st len f = n holds
f in the carrier of (Euclid n) by TOPREAL3:45;