let p be FinSequence; :: thesis: for A being finite set st p is one-to-one & A c= rng p holds
len (p - A) = (len p) - (card A)
let A be finite set ; :: thesis: ( p is one-to-one & A c= rng p implies len (p - A) = (len p) - (card A) )
assume that
A1: p is one-to-one and
A2: A c= rng p ; :: thesis: len (p - A) = (len p) - (card A)
A /\ (rng p) = A by A2, XBOOLE_1:28;
hence len (p - A) = (len p) - (card A) by A1, Th86; :: thesis: verum