let Y be set ; :: thesis: for p being FinSequence st ( for i being Nat st i in dom p holds

p . i in Y ) holds

p is FinSequence of Y

let p be FinSequence; :: thesis: ( ( for i being Nat st i in dom p holds

p . i in Y ) implies p is FinSequence of Y )

assume A1: for i being Nat st i in dom p holds

p . i in Y ; :: thesis: p is FinSequence of Y

let b be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not b in rng p or b in Y )

assume b in rng p ; :: thesis: b in Y

then ex i being Nat st

( i in dom p & p . i = b ) by FINSEQ_2:10;

hence b in Y by A1; :: thesis: verum

p . i in Y ) holds

p is FinSequence of Y

let p be FinSequence; :: thesis: ( ( for i being Nat st i in dom p holds

p . i in Y ) implies p is FinSequence of Y )

assume A1: for i being Nat st i in dom p holds

p . i in Y ; :: thesis: p is FinSequence of Y

let b be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not b in rng p or b in Y )

assume b in rng p ; :: thesis: b in Y

then ex i being Nat st

( i in dom p & p . i = b ) by FINSEQ_2:10;

hence b in Y by A1; :: thesis: verum