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