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_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[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

( f . d > 0 & f . d <= n ) ) & f is one-to-one holds

rng f = Seg n

defpred S

( f . d > 0 & f . d <= $1 ) ) & f is one-to-one holds

rng f = Seg $1;

A1: for n being Nat st S

S

proof

A51:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

S_{1}[n + 1]
_{1}[n + 1]
; :: thesis: verum

end;assume A2: S

S

proof

hence
S
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;

end;( 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;

end;

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 )

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;( f1 . d > 0 & f1 . d <= n )

proof

then
rng f1 = Seg n
by A2, A3, A11, A10;
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;

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

f . d <= n + 1
by A4, A15;
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;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

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

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

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 )

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 )

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;( d in dom f1 & f1 . d = n + 1 )

proof

then consider d1 being Element of NAT such that
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

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;f1 . d <> n + 1 ; :: thesis: contradiction

for d being Nat st d in dom f holds

f . d in Seg n

proof

then
f is FinSequence of Seg n
by FINSEQ_2:12;
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;

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

end;

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

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

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

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

f3 is one-to-one
by A36, A41, FINSEQ_3:91;
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;

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

(Swap (f,d1,(n + 1))) . d in rng (Swap (f,d1,(n + 1)))
by A44, FUNCT_1:3;
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;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

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

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

proof

for n being Nat holds S
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;( 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

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