let i, k be Nat; 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 ; for f being FinSequence of D st i + k = len f holds
Rev (f /^ k) = (Rev f) | i
let f be FinSequence of D; ( i + k = len f implies Rev (f /^ k) = (Rev f) | i )
assume A1:
i + k = len f
; Rev (f /^ k) = (Rev f) | i
then A2:
k <= len f
by NAT_1:11;
i <= len f
by A1, NAT_1:11;
then
i <= len (Rev f)
by FINSEQ_5:def 3;
then A3: len ((Rev f) | i) =
(len f) - k
by A1, FINSEQ_1:59
.=
len (f /^ k)
by A2, RFINSEQ:def 1
;
now for j being Nat st j in dom ((Rev f) | i) holds
((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1)A4:
len (f /^ k) = (len f) - k
by A2, RFINSEQ:def 1;
let j be
Nat;
( j in dom ((Rev f) | i) implies ((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1) )A5:
dom ((Rev f) | i) c= dom (Rev f)
by FINSEQ_5:18;
assume A6:
j in dom ((Rev f) | i)
;
((Rev f) | i) . j = (f /^ k) . (((len (f /^ k)) - j) + 1)then
j <= len (f /^ k)
by A3, FINSEQ_3:25;
then reconsider m =
(len (f /^ k)) - j as
Element of
NAT by INT_1:5;
j >= 1
by A6, FINSEQ_3:25;
then
(len (f /^ k)) - j <= (len (f /^ k)) - 1
by XREAL_1:10;
then A7:
((len (f /^ k)) - j) + 1
<= len (f /^ k)
by XREAL_1:19;
1
<= m + 1
by NAT_1:11;
then A8:
m + 1
in dom (f /^ k)
by A7, FINSEQ_3:25;
thus ((Rev f) | i) . j =
((Rev f) | i) /. j
by A6, PARTFUN1:def 6
.=
(Rev f) /. j
by A6, FINSEQ_4:70
.=
(Rev f) . j
by A6, A5, PARTFUN1:def 6
.=
f . ((((len (f /^ k)) + k) - j) + 1)
by A6, A5, A4, FINSEQ_5:def 3
.=
f . ((m + 1) + k)
.=
(f /^ k) . (((len (f /^ k)) - j) + 1)
by A2, A8, RFINSEQ:def 1
;
verum end;
hence
Rev (f /^ k) = (Rev f) | i
by A3, FINSEQ_5:def 3; verum