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))) )
assume A1: p is one-to-one ; :: thesis: len (p - A) = (len p) - (card (A /\ (rng p)))
A2: ( dom p = Seg (len p) & p " A c= dom p & Seg (len p) is finite ) by FINSEQ_1:def 3, RELAT_1:167;
p " A,A /\ (rng p) are_equipotent

proof

deffunc H₁( set ) -> set = p . $1;
consider f being Function such that
A3: dom f = p " A and
A4: for x being set 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 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: 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 & y in dom f ) and
A6: f . x = f . y ; :: thesis: x = y
( x in dom p & y in dom p & p . x = f . x & f . y = p . y ) by A2, A3, A4, A5;
hence x = y by A1, A6, FUNCT_1:def 8; :: 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 set ; :: 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 set such that
A7: y in dom f and
A8: f . y = x by FUNCT_1:def 5;
A9: p . y in A by A3, A7, FUNCT_1:def 13;
y in dom p by A3, A7, FUNCT_1:def 13;
then ( p . y in rng p & p . y = f . y ) by A3, A4, A7, FUNCT_1:def 5;
hence x in A /\ (rng p) by A8, A9, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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