let p be FinSequence; :: thesis: for x being object st p is one-to-one & rng p = {x} holds
len p = 1
let x be object ; :: 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 :: thesis: for y1, y2 being object holds
( not y1 in dom p or not y2 in dom p or not y1 <> y2 )
given y1, y2 being object 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; :: 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 object ; :: 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 object ; :: 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, Th20; :: thesis: verum