theorem Th40: :: JGRAPH_1:41

for f being FinSequence of (TOP-REAL 2) st 1 <= len f holds
( len (X_axis f) = len f & (X_axis f) . 1 = (f /. 1) `1 & (X_axis f) . (len f) = (f /. (len f)) `1 )