let p be FinSequence; :: thesis: for x being object st p is one-to-one & rng p = {x} holds
p = <*x*>
let x be object ; :: 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, Th94;
hence p = <*x*> by A2, FINSEQ_1:39; :: thesis: verum