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

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