let p be Function; :: thesis: ( dom p = Seg 1 implies p = <*(p . 1)*> )
assume A1: dom p = Seg 1 ; :: thesis: p = <*(p . 1)*>
then A3: rng p = {(p . 1)} by FINSEQ_1:2, FUNCT_1:4;
p is FinSequence-like by A1;
hence p = <*(p . 1)*> by A3, A1, FINSEQ_1:38; :: thesis: verum