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
A2: p - A = p * (Sgm ((Seg (len p)) \ (p " A))) by FINSEQ_1:def 3;
Sgm ((Seg (len p)) \ (p " A)) is one-to-one by Lm1, XBOOLE_1:36;
hence p - A is one-to-one by A1, A2; :: thesis: verum