theorem Th45: :: TOPREAL3:45

for n being Nat
for f being FinSequence of REAL st len f = n holds
f in the carrier of (Euclid n)