let i be Nat; for k being Element of NAT
for p being FinSequence st k in dom p holds
(Sgm (dom (Shift (p,i)))) . k = i + k
let k be Element of NAT ; for p being FinSequence st k in dom p holds
(Sgm (dom (Shift (p,i)))) . k = i + k
let p be FinSequence; ( k in dom p implies (Sgm (dom (Shift (p,i)))) . k = i + k )
assume A1:
k in dom p
; (Sgm (dom (Shift (p,i)))) . k = i + k
consider fs being FinSequence such that
A2:
dom fs = dom p
and
A3:
rng fs = dom (Shift (p,i))
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 Lm5;
reconsider fs = fs as FinSequence of NAT by A3, FINSEQ_1:def 4;
for n, m being Nat st 1 <= n & n < m & m <= len fs holds
fs . n < fs . m
proof
let n,
m be
Nat;
( 1 <= n & n < m & m <= len fs implies fs . n < fs . m )
assume that A6:
1
<= n
and A7:
n < m
and A8:
m <= len fs
;
fs . n < fs . m
set k1 =
fs . n;
set k2 =
fs . m;
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 Nat : ( 1 <= n1 & n1 <= len fs ) }
;
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:
fs . n = i + n
by A4, A13;
fs . m = i + m
by A4, A14;
hence
fs . n < fs . m
by A7, A15, XREAL_1:8;
verum
end;
then
fs = Sgm (dom (Shift (p,i)))
by A3, FINSEQ_1:def 14;
hence
(Sgm (dom (Shift (p,i)))) . k = i + k
by A1, A4; verum