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 )
A1: f is Function of (dom f),D by FINSEQ_2:26;
assume A2: f = <*a*> ; :: thesis: a in D
then 1 <= len f by FINSEQ_1:40;
then A3: 1 in dom f by FINSEQ_3:25;
f . 1 = a by A2;
hence a in D by A3, A1, FUNCT_2:5; :: thesis: verum