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 and
A5: y2 in dom p and
A6: y1 <> y2 ; :: thesis: contradiction
p . y2 in rng p by A5, FUNCT_1:def 3;
then A7: p . y2 = x by A2, TARSKI:def 1;
p . y1 in rng p by A4, FUNCT_1:def 3;
then p . y1 = x by A2, TARSKI:def 1;
hence contradiction by A1, A4, A5, A6, A7, FUNCT_1:def 4; :: thesis: verum

end;

set y = the Element of dom p;
A8: dom p <> {} by A2, RELAT_1:42;
A9: dom p = { the Element of dom p}

proof

thus dom p c= { the Element of dom p} :: according to XBOOLE_0:def 10 :: thesis: { the Element of dom p} c= dom p

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { the Element of dom p} or x in dom p )
the Element of dom p in dom p by A8;
hence ( not x in { the Element of dom p} 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 A9, Th22; :: thesis: verum