let p be Function; :: thesis: ( dom p = Seg 1 implies p = <*(p . 1)*> )
assume A1: dom p = Seg 1 ; :: thesis: p = <*(p . 1)*>
consider x being set such that
A2: x = p . 1 ;
A3: rng p = {x} by A2, A1, FINSEQ_1:2, FUNCT_1:4;
p is FinSequence-like by A1, FINSEQ_1:def 2;
then consider pp being FinSequence such that
A4: pp = p ;
thus p = <*(p . 1)*> by A2, A4, A3, A1, FINSEQ_1:38; :: thesis: verum