let n be Nat; :: thesis: for f being FinSequence of NAT st len f = n & ( for d being Nat st d in dom f holds
( f . d > 0 & f . d <= n ) ) & f is one-to-one holds
rng f = Seg n
defpred S₁[ Nat] means for f being FinSequence of NAT st len f = $1 & ( for d being Nat st d in dom f holds
( f . d > 0 & f . d <= $1 ) ) & f is one-to-one holds
rng f = Seg $1;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
S₁[n + 1]

proof

let f be FinSequence of NAT ; :: thesis: ( len f = n + 1 & ( for d being Nat st d in dom f holds
( f . d > 0 & f . d <= n + 1 ) ) & f is one-to-one implies rng f = Seg (n + 1) )
assume that
A3: len f = n + 1 and
A4: for d being Nat st d in dom f holds
( f . d > 0 & f . d <= n + 1 ) and
A5: f is one-to-one ; :: thesis: rng f = Seg (n + 1)
A6: f <> {} by A3;
then A7: n + 1 in dom f by A3, FINSEQ_5:6;
then A8: f . (n + 1) > 0 by A4;
consider f1 being FinSequence of NAT , a being Element of NAT such that
A9: f = f1 ^ <*a*> by A6, HILBERT2:4;
A10: f1 is one-to-one by A5, A9, FINSEQ_3:91;
A11: len f = (len f1) + 1 by A9, FINSEQ_2:16;
f . (n + 1) <= n + 1 by A4, A7;
then A12: a <= n + 1 by A3, A9, A11, FINSEQ_1:42;

per cases ( a = n + 1 or ( a > 0 & a < n + 1 ) ) by A3, A9, A11, A8, A12, FINSEQ_1:42, XXREAL_0:1;

suppose A13: a = n + 1 ; :: thesis: rng f = Seg (n + 1)

for d being Nat st d in dom f1 holds
( f1 . d > 0 & f1 . d <= n )

proof

let d be Nat; :: thesis: ( d in dom f1 implies ( f1 . d > 0 & f1 . d <= n ) )
assume A14: d in dom f1 ; :: thesis: ( f1 . d > 0 & f1 . d <= n )
then A15: d in dom f by A9, FINSEQ_2:15;

A16: now :: thesis: not f1 . d = n + 1

d <= n by A3, A11, A14, FINSEQ_3:25;
then d < n + 1 by XREAL_1:145;
then f . d <> f . (n + 1) by A5, A7, A15;
then A17: f1 . d <> f . (n + 1) by A9, A14, FINSEQ_1:def 7;
assume f1 . d = n + 1 ; :: thesis: contradiction
hence contradiction by A3, A9, A11, A13, A17, FINSEQ_1:42; :: thesis: verum

end;

f . d <= n + 1 by A4, A15;
then f1 . d <= n + 1 by A9, A14, FINSEQ_1:def 7;
then A18: f1 . d < n + 1 by A16, XXREAL_0:1;
f . d > 0 by A4, A15;
hence ( f1 . d > 0 & f1 . d <= n ) by A9, A14, A18, FINSEQ_1:def 7, NAT_1:13; :: thesis: verum

end;

then rng f1 = Seg n by A2, A3, A11, A10;
then (rng f1) \/ {a} = Seg (n + 1) by A13, FINSEQ_1:9;
then (rng f1) \/ (rng <*a*>) = Seg (n + 1) by FINSEQ_1:38;
hence rng f = Seg (n + 1) by A9, FINSEQ_1:31; :: thesis: verum

end;

suppose A19: ( a > 0 & a < n + 1 ) ; :: thesis: rng f = Seg (n + 1)

ex d being Nat st
( d in dom f1 & f1 . d = n + 1 )

proof

assume A20: for d being Nat st d in dom f1 holds
f1 . d <> n + 1 ; :: thesis: contradiction
for d being Nat st d in dom f holds
f . d in Seg n

proof

let d be Nat; :: thesis: ( d in dom f implies f . d in Seg n )
assume A21: d in dom f ; :: thesis: f . d in Seg n
then A22: d in Seg (n + 1) by A3, FINSEQ_1:def 3;
then A23: d <= n + 1 by FINSEQ_1:1;

per cases ( d = n + 1 or ( d >= 1 & d < n + 1 ) ) by A22, A23, FINSEQ_1:1, XXREAL_0:1;

suppose d = n + 1 ; :: thesis: f . d in Seg n

then A24: f . d = a by A3, A9, A11, FINSEQ_1:42;
then A25: f . d <= n by A19, NAT_1:13;
f . d >= 0 + 1 by A19, A24, NAT_1:13;
hence f . d in Seg n by A25, FINSEQ_1:1; :: thesis: verum

end;

suppose A26: ( d >= 1 & d < n + 1 ) ; :: thesis: f . d in Seg n

then d <= n by NAT_1:13;
then d in Seg n by A26, FINSEQ_1:1;
then A27: d in dom f1 by A3, A11, FINSEQ_1:def 3;
then f1 . d <> n + 1 by A20;
then A28: f . d <> n + 1 by A9, A27, FINSEQ_1:def 7;
f . d <= n + 1 by A4, A21;
then f . d < n + 1 by A28, XXREAL_0:1;
then A29: f . d <= n by NAT_1:13;
f . d > 0 by A4, A21;
then f . d >= 0 + 1 by NAT_1:13;
hence f . d in Seg n by A29, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

then f is FinSequence of Seg n by FINSEQ_2:12;
then rng f c= Seg n by FINSEQ_1:def 4;
then card (rng f) <= card (Seg n) by NAT_1:43;
then n + 1 <= card (Seg n) by A3, A5, FINSEQ_4:62;
then n + 1 <= n + 0 by FINSEQ_1:57;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

then consider d1 being Element of NAT such that
A30: d1 in dom f1 and
A31: f1 . d1 = n + 1 ;
d1 <= n by A3, A11, A30, FINSEQ_3:25;
then A32: d1 <= len f by A3, NAT_1:13;
A33: 0 + 1 <= n + 1 by XREAL_1:6;
set f2 = Swap (f,d1,(n + 1));
A34: len (Swap (f,d1,(n + 1))) = n + 1 by A3, FINSEQ_7:18;
then A35: Swap (f,d1,(n + 1)) <> {} ;
then consider f3 being FinSequence of NAT , b being Element of NAT such that
A36: Swap (f,d1,(n + 1)) = f3 ^ <*b*> by HILBERT2:4;
A37: n + 1 = (len f3) + 1 by A34, A36, FINSEQ_2:16;
A38: 1 <= d1 by A30, FINSEQ_3:25;
then (Swap (f,d1,(n + 1))) /. (n + 1) = f /. d1 by A3, A32, A33, FINSEQ_7:31;
then (Swap (f,d1,(n + 1))) /. (n + 1) = f . d1 by A38, A32, FINSEQ_4:15;
then (Swap (f,d1,(n + 1))) . (n + 1) = f . d1 by A34, A33, FINSEQ_4:15;
then A39: (Swap (f,d1,(n + 1))) . (n + 1) = n + 1 by A9, A30, A31, FINSEQ_1:def 7;
then A40: b = n + 1 by A36, A37, FINSEQ_1:42;
A41: Swap (f,d1,(n + 1)) is one-to-one by A5, Th39;
A42: for d being Nat st d in dom f3 holds
( f3 . d > 0 & f3 . d <= n )

proof

let d be Nat; :: thesis: ( d in dom f3 implies ( f3 . d > 0 & f3 . d <= n ) )
assume A43: d in dom f3 ; :: thesis: ( f3 . d > 0 & f3 . d <= n )
then A44: d in dom (Swap (f,d1,(n + 1))) by A36, FINSEQ_2:15;

A45: now :: thesis: not f3 . d = n + 1

d <= n by A37, A43, FINSEQ_3:25;
then A46: d < n + 1 by XREAL_1:145;
assume f3 . d = n + 1 ; :: thesis: contradiction
then A47: (Swap (f,d1,(n + 1))) . d = n + 1 by A36, A43, FINSEQ_1:def 7;
n + 1 in dom (Swap (f,d1,(n + 1))) by A34, A35, FINSEQ_5:6;
hence contradiction by A39, A41, A44, A47, A46; :: thesis: verum

end;

(Swap (f,d1,(n + 1))) . d in rng (Swap (f,d1,(n + 1))) by A44, FUNCT_1:3;
then (Swap (f,d1,(n + 1))) . d in rng f by FINSEQ_7:22;
then A48: ex e being Nat st
( e in dom f & (Swap (f,d1,(n + 1))) . d = f . e ) by FINSEQ_2:10;
then (Swap (f,d1,(n + 1))) . d <= n + 1 by A4;
then f3 . d <= n + 1 by A36, A43, FINSEQ_1:def 7;
then A49: f3 . d < n + 1 by A45, XXREAL_0:1;
(Swap (f,d1,(n + 1))) . d > 0 by A4, A48;
hence ( f3 . d > 0 & f3 . d <= n ) by A36, A43, A49, FINSEQ_1:def 7, NAT_1:13; :: thesis: verum

end;

f3 is one-to-one by A36, A41, FINSEQ_3:91;
then A50: rng f3 = Seg n by A2, A37, A42;
rng (Swap (f,d1,(n + 1))) = (rng f3) \/ (rng <*b*>) by A36, FINSEQ_1:31
.= (Seg n) \/ {(n + 1)} by A40, A50, FINSEQ_1:38
.= Seg (n + 1) by FINSEQ_1:9 ;
hence rng f = Seg (n + 1) by FINSEQ_7:22; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A51: S₁[ 0 ]

proof

let f be FinSequence of NAT ; :: thesis: ( len f = 0 & ( for d being Nat st d in dom f holds
( f . d > 0 & f . d <= 0 ) ) & f is one-to-one implies rng f = Seg 0 )
assume len f = 0 ; :: thesis: ( ex d being Nat st
( d in dom f & not ( f . d > 0 & f . d <= 0 ) ) or not f is one-to-one or rng f = Seg 0 )
then f = {} ;
hence ( ex d being Nat st
( d in dom f & not ( f . d > 0 & f . d <= 0 ) ) or not f is one-to-one or rng f = Seg 0 ) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A51, A1);
hence for f being FinSequence of NAT st len f = n & ( for d being Nat st d in dom f holds
( f . d > 0 & f . d <= n ) ) & f is one-to-one holds
rng f = Seg n ; :: thesis: verum