let p be FinSequence; :: thesis: for x being object st p is one-to-one & x in rng p holds
len (p - {x}) = (len p) - 1
let x be object ; :: 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:31;
then len (p - {x}) = (len p) - (card {x}) by A1, Th87;
hence len (p - {x}) = (len p) - 1 by CARD_1:30; :: thesis: verum