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 x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in D )
assume x in rng p ; :: thesis: x in D
then ex i being Element of NAT st
( i in dom p & p . i = x ) by Th3;
hence x in D by A1; :: thesis: verum

end;

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