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

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