let x be REAL -valued FinSequence; :: thesis: ( 1 <= len x implies dom (x | 1) = {1} )
assume 1 <= len x ; :: thesis: dom (x | 1) = {1}
then A3: len (x | 1) = 1 by FINSEQ_1:59;
1 in Seg 1 ;
then (x | 1) . 1 = x . 1 by FUNCT_1:49;
then x | 1 = <*(x . 1)*> by FINSEQ_1:40, A3;
hence dom (x | 1) = {1} by FINSEQ_1:2, FINSEQ_1:38; :: thesis: verum