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

hence p is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum

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

then
rng p c= D
;
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;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

hence p is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum