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, FINSEQ_1:40;

hence a in D by A3, A1, FUNCT_2:5; :: thesis: verum

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, FINSEQ_1:40;

hence a in D by A3, A1, FUNCT_2:5; :: thesis: verum