let x be set ; :: thesis: for p being XFinSequence st x in rng p holds
ex i being Element of NAT st
( i in dom p & p . i = x )
let p be XFinSequence; :: thesis: ( x in rng p implies ex i being Element of NAT st
( i in dom p & p . i = x ) )
assume x in rng p ; :: thesis: ex i being Element of NAT st
( i in dom p & p . i = x )
then ex a being set st
( a in dom p & x = p . a ) by FUNCT_1:def 5;
hence ex i being Element of NAT st
( i in dom p & p . i = x ) ; :: thesis: verum