let p be FinSequence; :: thesis: for x being set st p is one-to-one & x in rng p holds
len (p - {x}) = (len p) - 1
let x be set ; :: thesis: ( p is one-to-one & x in rng p implies len (p - {x}) = (len p) - 1 )
assume that
A1: p is one-to-one and
A2: x in rng p ; :: thesis: len (p - {x}) = (len p) - 1
{x} c= rng p by A2, ZFMISC_1:37;
then len (p - {x}) = (len p) - (card {x}) by A1, Th96;
hence len (p - {x}) = (len p) - 1 by CARD_1:50; :: thesis: verum