let k, i be Element of NAT ; for p being FinSequence st k in dom p holds
(Sgm (dom (i Shift p))) . k = i + k
let p be FinSequence; ( k in dom p implies (Sgm (dom (i Shift p))) . k = i + k )
assume A1:
k in dom p
; (Sgm (dom (i Shift p))) . k = i + k
consider fs being FinSequence such that
A2:
dom fs = dom p
and
A3:
rng fs = dom (i Shift p)
and
A4:
for j being Element of NAT st j in dom p holds
fs . j = i + j
and
fs is one-to-one
by Lm8;
A5:
ex l being Nat st dom (i Shift p) c= Seg l
by FINSEQ_1:def 12;
rng fs = rng (Sgm (dom (i Shift p)))
by A3, FINSEQ_1:50;
then reconsider fs = fs as FinSequence of NAT by FINSEQ_1:def 4;
for n, m, k1, k2 being natural number st 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m holds
k1 < k2
proof
let n,
m,
k1,
k2 be
natural number ;
( 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m implies k1 < k2 )
assume that A6:
1
<= n
and A7:
n < m
and A8:
m <= len fs
and A9:
k1 = fs . n
and A10:
k2 = fs . m
;
k1 < k2
reconsider n =
n,
m =
m as
Element of
NAT by ORDINAL1:def 12;
A11:
dom fs =
Seg (len fs)
by FINSEQ_1:def 3
.=
{ n1 where n1 is Element of NAT : ( 1 <= n1 & n1 <= len fs ) }
by FINSEQ_1:def 1
;
n + 1
<= m
by A7, INT_1:7;
then
n + 1
<= len fs
by A8, XXREAL_0:2;
then A12:
n <= (len fs) - 1
by XREAL_1:19;
(len fs) + 0 <= (len fs) + 1
by XREAL_1:7;
then
(len fs) - 1
<= len fs
by XREAL_1:20;
then
n <= len fs
by A12, XXREAL_0:2;
then A13:
n in dom p
by A2, A6, A11;
1
<= m
by A6, A7, XXREAL_0:2;
then A14:
m in dom p
by A2, A8, A11;
A15:
k1 = i + n
by A4, A9, A13;
k2 = i + m
by A4, A10, A14;
hence
k1 < k2
by A7, A15, XREAL_1:8;
verum
end;
then
fs = Sgm (dom (i Shift p))
by A3, A5, FINSEQ_1:def 13;
hence
(Sgm (dom (i Shift p))) . k = i + k
by A1, A4; verum