theorem :: EUCLID_3:22

for f being FinSequence of REAL st len f = 2 holds
|.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2))