let b be object ; :: thesis: for p being FinSequence st b in rng p holds
ex i being Nat st
( i in dom p & p . i = b )
let p be FinSequence; :: thesis: ( b in rng p implies ex i being Nat st
( i in dom p & p . i = b ) )
assume b in rng p ; :: thesis: ex i being Nat st
( i in dom p & p . i = b )
then ex a being object st
( a in dom p & b = p . a ) by FUNCT_1:def 3;
hence ex i being Nat st
( i in dom p & p . i = b ) ; :: thesis: verum