theorem :: EUCLID_8:2

for f being FinSequence of REAL st len f = 3 holds
f is Element of REAL 3