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

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: 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 A4: ( 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 ) ; :: thesis: rng f = Seg (n + 1)
then A5: f <> {} ;
then consider f1 being FinSequence of NAT , a being Element of NAT such that
A6: f = f1 ^ <*a*> by HILBERT2:4;
A7: len f = (len f1) + 1 by A6, FINSEQ_2:19;
A8: ( f1 is one-to-one & rng f1 misses rng <*a*> ) by A4, A6, FINSEQ_3:98;
A9: n + 1 in dom f by A4, A5, FINSEQ_5:6;
then ( f . (n + 1) > 0 & f . (n + 1) <= n + 1 ) by A4;
then A10: ( a > 0 & a <= n + 1 ) by A4, A6, A7, FINSEQ_1:59;

per cases ( a = n + 1 or ( a > 0 & a < n + 1 ) ) by A10, XXREAL_0:1;

suppose A11: 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 A12: d in dom f1 ; :: thesis: ( f1 . d > 0 & f1 . d <= n )
then A13: d in dom f by A6, FINSEQ_2:18;
then A14: ( f . d > 0 & f . d <= n + 1 ) by A4;
then A15: ( f1 . d > 0 & f1 . d <= n + 1 ) by A6, A12, FINSEQ_1:def 7;

now

assume A16: f1 . d = n + 1 ; :: thesis: contradiction
d <= n by A4, A7, A12, FINSEQ_3:27;
then d < n + 1 by XREAL_1:147;
then f . d <> f . (n + 1) by A4, A9, A13, FUNCT_1:def 8;
then f1 . d <> f . (n + 1) by A6, A12, FINSEQ_1:def 7;
hence contradiction by A4, A6, A7, A11, A16, FINSEQ_1:59; :: thesis: verum

end;

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

end;

then rng f1 = Seg n by A3, A4, A7, A8;
then (rng f1) \/ {a} = Seg (n + 1) by A11, FINSEQ_1:11;
then (rng f1) \/ (rng <*a*>) = Seg (n + 1) by FINSEQ_1:55;
hence rng f = Seg (n + 1) by A6, FINSEQ_1:44; :: thesis: verum

end;

suppose A17: ( 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 A18: 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 A19: d in dom f ; :: thesis: f . d in Seg n
then d in Seg (n + 1) by A4, FINSEQ_1:def 3;
then A20: ( d >= 1 & d <= n + 1 ) by FINSEQ_1:3;

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

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

then f . d = a by A4, A6, A7, FINSEQ_1:59;
then ( f . d >= 0 + 1 & f . d <= n ) by A17, NAT_1:13;
hence f . d in Seg n by FINSEQ_1:3; :: thesis: verum

end;

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

then ( d >= 1 & d <= n ) by NAT_1:13;
then d in Seg n by FINSEQ_1:3;
then A21: d in dom f1 by A4, A7, FINSEQ_1:def 3;
then f1 . d <> n + 1 by A18;
then A22: f . d <> n + 1 by A6, A21, FINSEQ_1:def 7;
( f . d > 0 & f . d <= n + 1 ) by A4, A19;
then ( f . d > 0 & f . d < n + 1 ) by A22, XXREAL_0:1;
then ( f . d >= 0 + 1 & f . d <= n ) by NAT_1:13;
hence f . d in Seg n by FINSEQ_1:3; :: thesis: verum

end;

end;

end;

then f is FinSequence of Seg n by FINSEQ_2:14;
then rng f c= Seg n by FINSEQ_1:def 4;
then card (rng f) <= card (Seg n) by NAT_1:44;
then n + 1 <= card (Seg n) by A4, FINSEQ_4:77;
then n + 1 <= n + 0 by FINSEQ_1:78;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then consider d1 being Element of NAT such that
A23: ( d1 in dom f1 & f1 . d1 = n + 1 ) ;
set f2 = Swap f,d1,(n + 1);
A24: len (Swap f,d1,(n + 1)) = n + 1 by A4, FINSEQ_7:20;
then A25: Swap f,d1,(n + 1) <> {} ;
then consider f3 being FinSequence of NAT , b being Element of NAT such that
A26: Swap f,d1,(n + 1) = f3 ^ <*b*> by HILBERT2:4;
A27: n + 1 = (len f3) + 1 by A24, A26, FINSEQ_2:19;
( d1 >= 1 & d1 <= n ) by A4, A7, A23, FINSEQ_3:27;
then A28: ( 1 <= d1 & d1 <= len f ) by A4, NAT_1:13;
A29: ( 0 + 1 <= n + 1 & n + 1 <= len f ) by A4, XREAL_1:8;
then (Swap f,d1,(n + 1)) /. (n + 1) = f /. d1 by A28, FINSEQ_7:33;
then (Swap f,d1,(n + 1)) /. (n + 1) = f . d1 by A28, FINSEQ_4:24;
then (Swap f,d1,(n + 1)) . (n + 1) = f . d1 by A24, A29, FINSEQ_4:24;
then A30: (Swap f,d1,(n + 1)) . (n + 1) = n + 1 by A6, A23, FINSEQ_1:def 7;
A31: Swap f,d1,(n + 1) is one-to-one by A4, Th39;
then A32: f3 is one-to-one by A26, FINSEQ_3:98;
A33: b = n + 1 by A26, A27, A30, FINSEQ_1:59;
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 A34: d in dom f3 ; :: thesis: ( f3 . d > 0 & f3 . d <= n )
then A35: d in dom (Swap f,d1,(n + 1)) by A26, FINSEQ_2:18;
then (Swap f,d1,(n + 1)) . d in rng (Swap f,d1,(n + 1)) by FUNCT_1:12;
then (Swap f,d1,(n + 1)) . d in rng f by FINSEQ_7:24;
then consider e being Nat such that
A36: ( e in dom f & (Swap f,d1,(n + 1)) . d = f . e ) by FINSEQ_2:11;
( (Swap f,d1,(n + 1)) . d > 0 & (Swap f,d1,(n + 1)) . d <= n + 1 ) by A4, A36;
then A37: ( f3 . d > 0 & f3 . d <= n + 1 ) by A26, A34, FINSEQ_1:def 7;

now

assume f3 . d = n + 1 ; :: thesis: contradiction
then A38: (Swap f,d1,(n + 1)) . d = n + 1 by A26, A34, FINSEQ_1:def 7;
d <= n by A27, A34, FINSEQ_3:27;
then A39: d < n + 1 by XREAL_1:147;
n + 1 in dom (Swap f,d1,(n + 1)) by A24, A25, FINSEQ_5:6;
hence contradiction by A30, A31, A35, A38, A39, FUNCT_1:def 8; :: thesis: verum

end;

then ( f3 . d > 0 & f3 . d < n + 1 ) by A37, XXREAL_0:1;
hence ( f3 . d > 0 & f3 . d <= n ) by NAT_1:13; :: thesis: verum

end;

then A40: rng f3 = Seg n by A3, A27, A32;
rng (Swap f,d1,(n + 1)) = (rng f3) \/ (rng <*b*>) by A26, FINSEQ_1:44
.= (Seg n) \/ {(n + 1)} by A33, A40, FINSEQ_1:55
.= Seg (n + 1) by FINSEQ_1:11 ;
hence rng f = Seg (n + 1) by FINSEQ_7:24; :: thesis: verum

end;

end;

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
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