let p be FinSequence; :: thesis: for x being set st p is one-to-one & rng p = {x} holds
len p = 1
let x be set ; :: thesis: ( p is one-to-one & rng p = {x} implies len p = 1 )
assume that
A1: p is one-to-one and
A2: rng p = {x} ; :: thesis: len p = 1

A3: now

given y1, y2 being set such that A4: ( y1 in dom p & y2 in dom p ) and
A5: y1 <> y2 ; :: thesis: contradiction
( p . y1 in rng p & p . y2 in rng p ) by A4, FUNCT_1:def 5;
then ( p . y1 = x & p . y2 = x ) by A2, TARSKI:def 1;
hence contradiction by A1, A4, A5, FUNCT_1:def 8; :: thesis: verum

end;

A6: dom p <> {} by A2, RELAT_1:65;
consider y being Element of dom p;
A7: dom p = {y}

proof

thus dom p c= {y} :: according to XBOOLE_0:def 10 :: thesis: {y} c= dom p

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in {y} )
assume x in dom p ; :: thesis: x in {y}
then x = y by A3;
hence x in {y} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {y} or x in dom p )
y in dom p by A6;
hence ( not x in {y} or x in dom p ) by TARSKI:def 1; :: thesis: verum

end;

dom p = Seg (len p) by FINSEQ_1:def 3;
hence len p = 1 by A7, Th22; :: thesis: verum