let p be FinSequence; :: thesis: for x being set st p is one-to-one & rng p = {x} holds
p = <*x*>
let x be set ; :: thesis: ( p is one-to-one & rng p = {x} implies p = <*x*> )
assume that
A1: p is one-to-one and
A2: rng p = {x} ; :: thesis: p = <*x*>
len p = 1 by A1, A2, Th105;
hence p = <*x*> by A2, FINSEQ_1:56; :: thesis: verum