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 <*x*> = {x} by FINSEQ_1:38;
( ( 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:91;
hence ( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one ) by A1, FINSEQ_3:93, ZFMISC_1:48, ZFMISC_1:50; :: thesis: verum