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

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