let i, k be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i
let D be non empty set ; :: thesis: for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i
let f be FinSequence of D; :: thesis: ( i + k = len f implies Rev (f /^ k) = (Rev f) | i )
assume A1:
i + k = len f
; :: thesis: Rev (f /^ k) = (Rev f) | i
then A2:
i <= len f
by NAT_1:11;
A3:
k <= len f
by A1, NAT_1:11;
i <= len (Rev f)
by A2, FINSEQ_5:def 3;
then A4: len ((Rev f) | i) =
(len f) - k
by A1, FINSEQ_1:80
.=
len (f /^ k)
by A3, RFINSEQ:def 2
;
now let j be
Nat;
:: thesis: ( j in dom ((Rev f) | i) implies ((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1) )assume A5:
j in dom ((Rev f) | i)
;
:: thesis: ((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1)A6:
dom ((Rev f) | i) c= dom (Rev f)
by FINSEQ_5:20;
A7:
len (f /^ k) = (len f) - k
by A3, RFINSEQ:def 2;
j <= len (f /^ k)
by A4, A5, FINSEQ_3:27;
then reconsider m =
(len (f /^ k)) - j as
Element of
NAT by INT_1:18;
A8:
1
<= m + 1
by NAT_1:11;
j >= 1
by A5, FINSEQ_3:27;
then
(len (f /^ k)) - j <= (len (f /^ k)) - 1
by XREAL_1:12;
then
((len (f /^ k)) - j) + 1
<= len (f /^ k)
by XREAL_1:21;
then A9:
m + 1
in dom (f /^ k)
by A8, FINSEQ_3:27;
thus ((Rev f) | i) . j =
((Rev f) | i) /. j
by A5, PARTFUN1:def 8
.=
(Rev f) /. j
by A5, FINSEQ_4:85
.=
(Rev f) . j
by A5, A6, PARTFUN1:def 8
.=
f . ((((len (f /^ k)) + k) - j) + 1)
by A5, A6, A7, FINSEQ_5:def 3
.=
f . ((m + 1) + k)
.=
(f /^ k) . (((len (f /^ k)) - j) + 1)
by A3, A9, RFINSEQ:def 2
;
:: thesis: verum end;
hence
Rev (f /^ k) = (Rev f) | i
by A4, FINSEQ_5:def 3; :: thesis: verum