let D be set ; :: thesis: for p being XFinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is XFinSequence of D
let p be XFinSequence; :: thesis: ( ( for i being Nat st i in dom p holds
p . i in D ) implies p is XFinSequence of D )
assume A1: for i being Nat st i in dom p holds
p . i in D ; :: thesis: p is XFinSequence of D
rng p c= D

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng p or b in D )
assume b in rng p ; :: thesis: b in D
then ex i being Element of NAT st
( i in dom p & p . i = b ) by Th3;
hence b in D by A1; :: thesis: verum

end;

hence p is XFinSequence of D by RELAT_1:def 19; :: thesis: verum