let a be set ; :: thesis: for D being non empty set
for f being FinSequence of D st f = <*a*> holds
a in D
let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a*> holds
a in D
let f be FinSequence of D; :: thesis: ( f = <*a*> implies a in D )
assume A1: f = <*a*> ; :: thesis: a in D
then A2: ( len f = 1 & f . 1 = a ) by FINSEQ_1:57;
1 <= len f by A1, FINSEQ_1:57;
then A3: 1 in dom f by FINSEQ_3:27;
f is Function of dom f,D by FINSEQ_2:30;
hence a in D by A2, A3, FUNCT_2:7; :: thesis: verum