let D be set ; :: thesis: for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D
let p be FinSequence; :: thesis: ( ( for i being Nat st i in dom p holds
p . i in D ) implies p is FinSequence of D )
assume L000: for i being Nat st i in dom p holds
p . i in D ; :: thesis: p is FinSequence of D
for y being object st y in rng p holds
y in D

proof

let y1 be object ; :: thesis: ( y1 in rng p implies y1 in D )
assume L430: y1 in rng p ; :: thesis: y1 in D
consider i being object such that
L431: i in dom p and
L432: y1 = p . i by L430, FUNCT_1:def 3;
thus y1 in D by L431, L000, L432; :: thesis: verum

end;

then rng p c= D ;
hence p is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum