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