let p be FinSequence; :: thesis: for A being set st p is one-to-one holds
len (p - A) = (len p) - (card (A /\ (rng p)))
let A be set ; :: thesis: ( p is one-to-one implies len (p - A) = (len p) - (card (A /\ (rng p))) )
A1: p " A c= dom p by RELAT_1:132;
assume A2: p is one-to-one ; :: thesis: len (p - A) = (len p) - (card (A /\ (rng p)))
p " A,A /\ (rng p) are_equipotent

proof

deffunc H₁( object ) -> set = p . $1;
consider f being Function such that
A3: dom f = p " A and
A4: for x being object st x in p " A holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = p " A & rng f = A /\ (rng p) )
thus f is one-to-one :: thesis: ( dom f = p " A & rng f = A /\ (rng p) )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A5: x in dom f and
A6: y in dom f and
A7: f . x = f . y ; :: thesis: x = y
A8: f . y = p . y by A3, A4, A6;
p . x = f . x by A3, A4, A5;
hence x = y by A2, A1, A3, A5, A6, A7, A8; :: thesis: verum

end;

thus dom f = p " A by A3; :: thesis: rng f = A /\ (rng p)
thus rng f c= A /\ (rng p) :: according to XBOOLE_0:def 10 :: thesis: A /\ (rng p) c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in A /\ (rng p) )
assume x in rng f ; :: thesis: x in A /\ (rng p)
then consider y being object such that
A9: y in dom f and
A10: f . y = x by FUNCT_1:def 3;
A11: p . y in A by A3, A9, FUNCT_1:def 7;
y in dom p by A3, A9, FUNCT_1:def 7;
then A12: p . y in rng p by FUNCT_1:def 3;
p . y = f . y by A3, A4, A9;
hence x in A /\ (rng p) by A10, A11, A12, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ (rng p) or x in rng f )
assume A13: x in A /\ (rng p) ; :: thesis: x in rng f
then x in rng p by XBOOLE_0:def 4;
then consider y being object such that
A14: y in dom p and
A15: p . y = x by FUNCT_1:def 3;
p . y in A by A13, A15, XBOOLE_0:def 4;
then A16: y in p " A by A14, FUNCT_1:def 7;
then f . y = x by A4, A15;
hence x in rng f by A3, A16, FUNCT_1:def 3; :: thesis: verum

end;

then card (p " A) = card (A /\ (rng p)) by CARD_1:5;
hence len (p - A) = (len p) - (card (A /\ (rng p))) by Th57; :: thesis: verum