let p be Function; :: thesis: ( dom p = Seg 1 implies p = <*(p . 1)*> )
assume AS: dom p = Seg 1 ; :: thesis: p = <*(p . 1)*>
consider x being set such that
L1: x = p . 1 ;
L2: rng p = {x} by L1, FUNCT_1:14, FINSEQ_1:4, AS;
p is FinSequence-like by FINSEQ_1:def 2, AS;
then consider pp being FinSequence such that
L3: pp = p ;
thus p = <*(p . 1)*> by L1, L3, FINSEQ_1:55, L2, AS; :: thesis: verum