let p be FinSequence; :: thesis: for x being set st x in rng p holds
x .. p in p " {x}
let x be set ; :: thesis: ( x in rng p implies x .. p in p " {x} )
assume x in rng p ; :: thesis: x .. p in p " {x}
then ( p . (x .. p) = x & x .. p in dom p ) by Th29, Th30;
then ( p . (x .. p) in {x} & x .. p in dom p ) by TARSKI:def 1;
hence x .. p in p " {x} by FUNCT_1:def 13; :: thesis: verum