let p be FinSequence; :: thesis: for D being set st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D
let D be set ; :: thesis: ( ( for i being Nat st i in dom p holds
p . i in D ) implies p is FinSequence of D )
assume A1: for i being Nat st i in dom p holds
p . i in D ; :: thesis: p is FinSequence of D
let b be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not b in rng p or b in D )
assume b in rng p ; :: thesis: b in D
then ex i being Nat st
( i in dom p & p . i = b ) by Th8;
hence b in D by A1; :: thesis: verum