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;
A5:
ex l being Nat st dom (Shift (p,i)) c= Seg l
by FINSEQ_1:def 12;
reconsider fs = fs as FinSequence of NAT by A3, FINSEQ_1:def 4;
for n, m, k1, k2 being Nat st 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m holds
k1 < k2
proof
let n,
m,
k1,
k2 be
Nat;
( 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 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:
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 (Shift (p,i)))
by A3, A5, FINSEQ_1:def 13;
hence
(Sgm (dom (Shift (p,i)))) . k = i + k
by A1, A4; verum