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:30;
assume A2: f = <*a*> ; :: thesis: a in D
then 1 <= len f by FINSEQ_1:57;
then A3: 1 in dom f by FINSEQ_3:27;
f . 1 = a by A2, FINSEQ_1:57;
hence a in D by A3, A1, FUNCT_2:7; :: thesis: verum