let D be non empty set ; 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; ( 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
; 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
; ( 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; 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; verum