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 A1: x in rng p ; :: thesis: x .. p in p " {x}
then p . (x .. p) = x by Th29;
then A2: p . (x .. p) in {x} by TARSKI:def 1;
x .. p in dom p by A1, Th30;
hence x .. p in p " {x} by A2, FUNCT_1:def 13; :: thesis: verum