defpred S1[ Nat] means for f being FinSequence of NAT
for n being Nat st len f = $1 & rng f c= Seg n & f is one-to-one & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = f;
A1:
S1[ 0 ]
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let f be
FinSequence of
NAT ;
for n being Nat st len f = n + 1 & rng f c= Seg n & f is one-to-one & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = flet k be
Nat;
( len f = n + 1 & rng f c= Seg k & f is one-to-one & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) implies Sgm (rng f) = f )
assume that A5:
len f = n + 1
and A6:
rng f c= Seg k
and A7:
f is
one-to-one
and A8:
for
i,
j being
Nat st
i in dom f &
j in dom f &
i < j holds
f . i < f . j
;
Sgm (rng f) = f
set fn =
f | n;
A9:
f = (f | n) ^ <*(f . (n + 1))*>
by A5, FINSEQ_3:55;
then A10:
rng (f | n) c= rng f
by FINSEQ_1:29;
A11:
dom (f | n) c= dom f
by A9, FINSEQ_1:26;
A12:
for
i,
j being
Nat st
i in dom (f | n) &
j in dom (f | n) &
i < j holds
(f | n) . i < (f | n) . j
A15:
len (f | n) = n
by A5, FINSEQ_3:53;
A16:
now for m9, n9 being Nat st m9 in rng (f | n) & n9 in {(f . (n + 1))} holds
m9 < n9A17:
(
n + 1
in Seg (n + 1) &
dom f = Seg (n + 1) )
by A5, FINSEQ_1:4, FINSEQ_1:def 3;
let m9,
n9 be
Nat;
( m9 in rng (f | n) & n9 in {(f . (n + 1))} implies m9 < n9 )assume that A18:
m9 in rng (f | n)
and A19:
n9 in {(f . (n + 1))}
;
m9 < n9consider x being
object such that A20:
x in dom (f | n)
and A21:
(f | n) . x = m9
by A18, FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A20;
A22:
f . x = (f | n) . x
by A9, A20, FINSEQ_1:def 7;
dom (f | n) = Seg n
by A15, FINSEQ_1:def 3;
then
x <= n
by A20, FINSEQ_1:1;
then
x < n + 1
by NAT_1:13;
then
f . x < f . (n + 1)
by A8, A11, A20, A17;
hence
m9 < n9
by A19, A21, A22, TARSKI:def 1;
verum end;
f | n is
one-to-one
by A7, FUNCT_1:52;
then A23:
Sgm (rng (f | n)) = f | n
by A4, A6, A15, A10, A12, XBOOLE_1:1;
A24:
rng <*(f . (n + 1))*> = {(f . (n + 1))}
by FINSEQ_1:39;
rng <*(f . (n + 1))*> c= rng f
by A9, FINSEQ_1:30;
then A25:
{(f . (n + 1))} c= Seg k
by A6, A24;
A26:
rng f = (rng (f | n)) \/ (rng <*(f . (n + 1))*>)
by A9, FINSEQ_1:31;
A27:
f . (n + 1) in {(f . (n + 1))}
by TARSKI:def 1;
rng (f | n) c= Seg k
by A6, A10;
hence Sgm (rng f) =
(f | n) ^ (Sgm {(f . (n + 1))})
by A26, A24, A25, A23, A16, FINSEQ_3:42
.=
f
by A9, A25, A27, FINSEQ_3:44
;
verum
end;
let f be FinSequence of NAT ; for n being Nat st f is one-to-one & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = f
let n be Nat; ( f is one-to-one & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) implies Sgm (rng f) = f )
assume A28:
( f is one-to-one & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) )
; Sgm (rng f) = f
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
then
for g being FinSequence of NAT
for n being Nat st len g = len f & rng g c= Seg n & g is one-to-one & ( for i, j being Nat st i in dom g & j in dom g & i < j holds
g . i < g . j ) holds
Sgm (rng g) = g
;
hence
Sgm (rng f) = f
by A28; verum