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