let p be FinSequence; :: thesis: ( rng p = dom p implies p is one-to-one )
defpred S₁[ 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 :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

set x = k + 1;
let p be FinSequence; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: contradiction
A13: 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; :: thesis: 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; :: thesis: verum

end;

end;

A20: S₁[ 0 ]

proof

let p be FinSequence; :: thesis: ( len p = 0 & rng p = dom p implies p is one-to-one )
assume len p = 0 ; :: thesis: ( not rng p = dom p or p is one-to-one )
then p = {} ;
hence ( not rng p = dom p or p is one-to-one ) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A20, A2);
hence ( rng p = dom p implies p is one-to-one ) by A1; :: thesis: verum