let D be non empty set ; :: thesis: for f being trivial FinSequence of D holds

( f is empty or ex x being Element of D st f = <*x*> )

let f be trivial FinSequence of D; :: thesis: ( f is empty or ex x being Element of D st f = <*x*> )

A1: rng f c= D by FINSEQ_1:def 4;

assume not f is empty ; :: thesis: ex x being Element of D st f = <*x*>

then consider x being object such that

A2: f = {x} by ZFMISC_1:131;

A3: 1 in dom f by A2, FINSEQ_5:6;

A4: x in {x} by TARSKI:def 1;

then consider y, z being object such that

A5: x = [y,z] by A2, RELAT_1:def 1;

reconsider z = z as set by TARSKI:1;

take z ; :: thesis: ( z is Element of D & f = <*z*> )

z in rng f by A2, A4, A5, XTUPLE_0:def 13;

hence z is Element of D by A1; :: thesis: f = <*z*>

dom f = {y} by A2, A5, RELAT_1:9;

then 1 = y by A3, TARSKI:def 1;

hence f = <*z*> by A2, A5; :: thesis: verum

( f is empty or ex x being Element of D st f = <*x*> )

let f be trivial FinSequence of D; :: thesis: ( f is empty or ex x being Element of D st f = <*x*> )

A1: rng f c= D by FINSEQ_1:def 4;

assume not f is empty ; :: thesis: ex x being Element of D st f = <*x*>

then consider x being object such that

A2: f = {x} by ZFMISC_1:131;

A3: 1 in dom f by A2, FINSEQ_5:6;

A4: x in {x} by TARSKI:def 1;

then consider y, z being object such that

A5: x = [y,z] by A2, RELAT_1:def 1;

reconsider z = z as set by TARSKI:1;

take z ; :: thesis: ( z is Element of D & f = <*z*> )

z in rng f by A2, A4, A5, XTUPLE_0:def 13;

hence z is Element of D by A1; :: thesis: f = <*z*>

dom f = {y} by A2, A5, RELAT_1:9;

then 1 = y by A3, TARSKI:def 1;

hence f = <*z*> by A2, A5; :: thesis: verum