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

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