let f be FinSequence of (TOP-REAL 2); :: thesis: ( 1 <= len f implies ( len (X_axis f) = len f & (X_axis f) . 1 = (f /. 1) `1 & (X_axis f) . (len f) = (f /. (len f)) `1 ) )
A1: len (X_axis f) = len f by GOBOARD1:def 1;
assume A2: 1 <= len f ; :: thesis: ( len (X_axis f) = len f & (X_axis f) . 1 = (f /. 1) `1 & (X_axis f) . (len f) = (f /. (len f)) `1 )
then len f in Seg (len f) by FINSEQ_1:1;
then A3: len f in dom (X_axis f) by A1, FINSEQ_1:def 3;
1 in Seg (len f) by A2, FINSEQ_1:1;
then 1 in dom (X_axis f) by A1, FINSEQ_1:def 3;
hence ( len (X_axis f) = len f & (X_axis f) . 1 = (f /. 1) `1 & (X_axis f) . (len f) = (f /. (len f)) `1 ) by A3, GOBOARD1:def 1; :: thesis: verum