let p be FinSequence; :: thesis: for x being object st x in rng p holds
x .. p in p " {x}
let x be object ; :: 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 Th19;
then A2: p . (x .. p) in {x} by TARSKI:def 1;
x .. p in dom p by A1, Th20;
hence x .. p in p " {x} by A2, FUNCT_1:def 7; :: thesis: verum