let f be trivial FinSequence; :: thesis: ( f is empty or ex x being object st f = <*x*> )
assume not f is empty ; :: thesis: ex x being object st f = <*x*>
then consider x being object such that
A1: f = {x} by ZFMISC_1:131;
x in {x} by TARSKI:def 1;
then consider y, z being object such that
A2: x = [y,z] by A1, RELAT_1:def 1;
A3: 1 in dom f by A1, FINSEQ_5:6;
take z ; :: thesis: f = <*z*>
dom f = {y} by A1, A2, RELAT_1:9;
then 1 = y by A3, TARSKI:def 1;
hence f = <*z*> by A1, A2, FINSEQ_1:def 5; :: thesis: verum