let p be FinSequence; :: thesis: for A being set st p is one-to-one holds
p - A is one-to-one
let A be set ; :: thesis: ( p is one-to-one implies p - A is one-to-one )
assume A1: p is one-to-one ; :: thesis: p - A is one-to-one
(Seg (len p)) \ (p " A) c= Seg (len p) by XBOOLE_1:36;
then ( p - A = p * (Sgm ((Seg (len p)) \ (p " A))) & Sgm ((Seg (len p)) \ (p " A)) is one-to-one ) by Lm1, FINSEQ_1:def 3;
hence p - A is one-to-one by A1; :: thesis: verum