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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
S1[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 ;
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 ;
A10: f1 is one-to-one by ;
A11: len f = (len f1) + 1 by ;
f . (n + 1) <= n + 1 by A4, A7;
then A12: a <= n + 1 by ;
per cases ( a = n + 1 or ( a > 0 & a < n + 1 ) ) by ;
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 ;
A16: now :: thesis: not f1 . d = n + 1
d <= n by ;
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 ;
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 ;
then f1 . d <= n + 1 by ;
then A18: f1 . d < n + 1 by ;
f . d > 0 by ;
hence ( f1 . d > 0 & f1 . d <= n ) by ; :: thesis: verum
end;
then rng f1 = Seg n by A2, A3, A11, A10;
then (rng f1) \/ {a} = Seg (n + 1) by ;
then (rng f1) \/ () = Seg (n + 1) by FINSEQ_1:38;
hence rng f = Seg (n + 1) by ; :: 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 ;
then A23: d <= n + 1 by FINSEQ_1:1;
per cases ( d = n + 1 or ( d >= 1 & d < n + 1 ) ) by ;
suppose d = n + 1 ; :: thesis: f . d in Seg n
then A24: f . d = a by ;
then A25: f . d <= n by ;
f . d >= 0 + 1 by ;
hence f . d in Seg n by ; :: 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 ;
then A27: d in dom f1 by ;
then f1 . d <> n + 1 by A20;
then A28: f . d <> n + 1 by ;
f . d <= n + 1 by ;
then f . d < n + 1 by ;
then A29: f . d <= n by NAT_1:13;
f . d > 0 by ;
then f . d >= 0 + 1 by NAT_1:13;
hence f . d in Seg n by ; :: 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 ;
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 ;
then A32: d1 <= len f by ;
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 ;
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 ;
A38: 1 <= d1 by ;
then (Swap (f,d1,(n + 1))) /. (n + 1) = f /. d1 by ;
then (Swap (f,d1,(n + 1))) /. (n + 1) = f . d1 by ;
then (Swap (f,d1,(n + 1))) . (n + 1) = f . d1 by ;
then A39: (Swap (f,d1,(n + 1))) . (n + 1) = n + 1 by ;
then A40: b = n + 1 by ;
A41: Swap (f,d1,(n + 1)) is one-to-one by ;
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 ;
A45: now :: thesis: not f3 . d = n + 1
d <= n by ;
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 ;
n + 1 in dom (Swap (f,d1,(n + 1))) by ;
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 ;
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 ;
then A49: f3 . d < n + 1 by ;
(Swap (f,d1,(n + 1))) . d > 0 by ;
hence ( f3 . d > 0 & f3 . d <= n ) by ; :: thesis: verum
end;
f3 is one-to-one by ;
then A50: rng f3 = Seg n by A2, A37, A42;
rng (Swap (f,d1,(n + 1))) = (rng f3) \/ () by
.= (Seg n) \/ {(n + 1)} by
.= Seg (n + 1) by FINSEQ_1:9 ;
hence rng f = Seg (n + 1) by FINSEQ_7:22; :: thesis: verum
end;
end;
end;
hence S1[n + 1] ; :: thesis: verum
end;
A51: S1[ 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 S1[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