theorem :: ANPROJ_8:79

for p being FinSequence of REAL st len p = 3 holds
p is 3 -element FinSequence of REAL