let p be FinSequence; :: thesis: for x being set holds
( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one )
let x be set ; :: thesis: ( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one )
A1: ( ( rng p misses rng <*x*> & p is one-to-one & <*x*> is one-to-one ) iff p ^ <*x*> is one-to-one ) by FINSEQ_3:98;
rng <*x*> = {x} by FINSEQ_1:55;
hence ( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one ) by A1, FINSEQ_3:102, ZFMISC_1:54, ZFMISC_1:56; :: thesis: verum