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: 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;

A2: now

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

let p be FinSequence; :: thesis: ( len p = k + 1 & rng p = dom p implies p is one-to-one )
set q = p - {(k + 1)};
set x = 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:6;

now

let l be Nat; :: thesis: ( l in dom p & l <> (k + 1) .. p implies not p . l = k + 1 )
assume that
A8: l in dom p and
A9: l <> (k + 1) .. p and
A10: p . l = k + 1 ; :: thesis: contradiction
p . ((k + 1) .. p) = k + 1 by A5, A6, Th29, FINSEQ_1:6;
then ( (k + 1) .. p in dom p & p . ((k + 1) .. p) in {(k + 1)} & p . l in {(k + 1)} ) by A7, A10, Th30, TARSKI:def 1;
then ( (k + 1) .. p in p " {(k + 1)} & l in p " {(k + 1)} ) by A8, FUNCT_1:def 13;
then A11: {((k + 1) .. p),l} c= p " {(k + 1)} by ZFMISC_1:38;
( card {((k + 1) .. p),l} = 2 & p " {(k + 1)} is finite ) by A9, CARD_2:76;
then ( 2 <= card (p " {(k + 1)}) & len (p - {(k + 1)}) = (k + 1) - (card (p " {(k + 1)})) ) by A4, A11, FINSEQ_3:66, NAT_1:44;
then 2 + (len (p - {(k + 1)})) <= (card (p " {(k + 1)})) + ((k + 1) - (card (p " {(k + 1)}))) by XREAL_1:8;
then ((len (p - {(k + 1)})) + 1) + 1 <= k + 1 ;
then (len (p - {(k + 1)})) + 1 <= k by XREAL_1:8;
then A12: ( len (p - {(k + 1)}) <= k - 1 & dom (p - {(k + 1)}) = Seg (len (p - {(k + 1)})) ) by FINSEQ_1:def 3, XREAL_1:21;
rng (p - {(k + 1)}) = (Seg (k + 1)) \ {(k + 1)} by A5, A6, FINSEQ_3:72
.= Seg k by FINSEQ_1:12 ;
then A13: card (rng (p - {(k + 1)})) = k by FINSEQ_1:78;
A14: card (rng (p - {(k + 1)})) c= card (dom (p - {(k + 1)})) by CARD_1:28;
( card (len (p - {(k + 1)})) = card (dom (p - {(k + 1)})) & card k = card (rng (p - {(k + 1)})) ) by A12, A13, FINSEQ_1:78;
then k <= len (p - {(k + 1)}) by A14, NAT_1:41;
then k <= k - 1 by A12, XXREAL_0:2;
then k + 1 <= k + 0 by XREAL_1:21;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then A15: p just_once_values k + 1 by A7, Th37;
then A16: len (p - {(k + 1)}) = (k + 1) - 1 by A4, Th40
.= k ;
A17: p - {(k + 1)} = (p -| (k + 1)) ^ (p |-- (k + 1)) by A15, Th69;
rng (p - {(k + 1)}) = (Seg (k + 1)) \ {(k + 1)} by A5, A6, FINSEQ_3:72
.= Seg k by FINSEQ_1:12 ;
then dom (p - {(k + 1)}) = rng (p - {(k + 1)}) by A16, FINSEQ_1:def 3;
hence p is one-to-one by A3, A7, A16, A17, Th71; :: thesis: verum

end;

end;

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