let p be non empty trivial XFinSequence; :: thesis: ex x being object st p = <%x%>
consider x being object such that
A1: rng p = {x} by ZFMISC_1:131;
take x ; :: thesis: p = <%x%>
consider z being object such that
A2: dom p = {z} by ZFMISC_1:131;
dom p = card {z} by A2;
then A3: dom p = 1 by CARD_1:30;
p = (dom p) --> x by A1, FUNCOP_1:9
.= 0 .--> x by A3, CARD_1:49, FUNCOP_1:def 9 ;
hence p = <%x%> by AFINSQ_1:def 1; :: thesis: verum