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

( ( 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