let p be FinSequence; ( rng p = dom p implies p is one-to-one )
defpred S1[ Nat] means for p being FinSequence st len p = $1 & rng p = dom p holds
p is one-to-one ;
A1:
len p = len p
;
A2:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A3:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
set x =
k + 1;
let p be
FinSequence;
( len p = k + 1 & rng p = dom p implies p is one-to-one )
set q =
p - {(k + 1)};
assume that A4:
len p = k + 1
and A5:
rng p = dom p
;
p is one-to-one
A6:
dom p = Seg (k + 1)
by A4, FINSEQ_1:def 3;
then A7:
k + 1
in rng p
by A5, FINSEQ_1:4;
now for l being Nat st l in dom p & l <> (k + 1) .. p holds
not p . l = k + 1 rng (p - {(k + 1)}) =
(Seg (k + 1)) \ {(k + 1)}
by A5, A6, FINSEQ_3:65
.=
Seg k
by FINSEQ_1:10
;
then
card (rng (p - {(k + 1)})) = k
by FINSEQ_1:57;
then A8:
card k = card (rng (p - {(k + 1)}))
;
p . ((k + 1) .. p) = k + 1
by A5, A6, Th19, FINSEQ_1:4;
then A9:
p . ((k + 1) .. p) in {(k + 1)}
by TARSKI:def 1;
let l be
Nat;
( l in dom p & l <> (k + 1) .. p implies not p . l = k + 1 )assume that A10:
l in dom p
and A11:
l <> (k + 1) .. p
and A12:
p . l = k + 1
;
contradictionA13:
card {((k + 1) .. p),l} = 2
by A11, CARD_2:57;
p . l in {(k + 1)}
by A12, TARSKI:def 1;
then A14:
l in p " {(k + 1)}
by A10, FUNCT_1:def 7;
(k + 1) .. p in dom p
by A5, A6, Th20, FINSEQ_1:4;
then
(k + 1) .. p in p " {(k + 1)}
by A9, FUNCT_1:def 7;
then
{((k + 1) .. p),l} c= p " {(k + 1)}
by A14, ZFMISC_1:32;
then A15:
2
<= card (p " {(k + 1)})
by A13, NAT_1:43;
len (p - {(k + 1)}) = (k + 1) - (card (p " {(k + 1)}))
by A4, FINSEQ_3:59;
then
2
+ (len (p - {(k + 1)})) <= (card (p " {(k + 1)})) + ((k + 1) - (card (p " {(k + 1)})))
by A15, XREAL_1:6;
then
((len (p - {(k + 1)})) + 1) + 1
<= k + 1
;
then
(len (p - {(k + 1)})) + 1
<= k
by XREAL_1:6;
then A16:
len (p - {(k + 1)}) <= k - 1
by XREAL_1:19;
dom (p - {(k + 1)}) = Seg (len (p - {(k + 1)}))
by FINSEQ_1:def 3;
then
(
card (Segm k) c= card (dom (p - {(k + 1)})) &
card (Segm (len (p - {(k + 1)}))) = card (dom (p - {(k + 1)})) )
by CARD_1:12, FINSEQ_1:57, A8;
then
k <= len (p - {(k + 1)})
by NAT_1:40;
then
k <= k - 1
by A16, XXREAL_0:2;
then
k + 1
<= k + 0
by XREAL_1:19;
hence
contradiction
by XREAL_1:6;
verum end;
then A17:
p just_once_values k + 1
by A7, Th27;
then A18:
len (p - {(k + 1)}) =
(k + 1) - 1
by A4, Th30
.=
k
;
A19:
p - {(k + 1)} = (p -| (k + 1)) ^ (p |-- (k + 1))
by A17, Th54;
rng (p - {(k + 1)}) =
(Seg (k + 1)) \ {(k + 1)}
by A5, A6, FINSEQ_3:65
.=
Seg k
by FINSEQ_1:10
;
then
dom (p - {(k + 1)}) = rng (p - {(k + 1)})
by A18, FINSEQ_1:def 3;
hence
p is
one-to-one
by A3, A7, A18, A19, Th56;
verum
end; end;
A20:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A20, A2);
hence
( rng p = dom p implies p is one-to-one )
by A1; verum