let x be set ; for f being FinSequence st f just_once_values x holds
Rev (f -| x) = (Rev f) |-- x
let f be FinSequence; ( f just_once_values x implies Rev (f -| x) = (Rev f) |-- x )
A1:
len (Rev (f -| x)) = len (f -| x)
by FINSEQ_5:def 3;
assume A2:
f just_once_values x
; Rev (f -| x) = (Rev f) |-- x
then A3:
x in rng f
by FINSEQ_4:5;
then A4:
x in rng (Rev f)
by FINSEQ_5:57;
A5:
(x .. f) + (x .. (Rev f)) = (len f) + 1
by A2, Th37;
A6:
now for k being Nat st k in dom (Rev (f -| x)) holds
(Rev (f -| x)) . k = (Rev f) . (k + (x .. (Rev f)))let k be
Nat;
( k in dom (Rev (f -| x)) implies (Rev (f -| x)) . k = (Rev f) . (k + (x .. (Rev f))) )consider m being
Nat such that
m = (x .. f) - 1
and A7:
f -| x = f | (Seg m)
by A3, FINSEQ_4:def 5;
assume A8:
k in dom (Rev (f -| x))
;
(Rev (f -| x)) . k = (Rev f) . (k + (x .. (Rev f)))then A9:
1
<= k
by FINSEQ_3:25;
then A10:
(x .. f) - k <= (x .. f) - 1
by XREAL_1:13;
A11:
len (f -| x) = (x .. f) - 1
by A3, FINSEQ_4:34;
k in dom (f -| x)
by A8, FINSEQ_5:57;
then
k <= (x .. f) - 1
by A11, FINSEQ_3:25;
then A12:
k + 1
<= x .. f
by XREAL_1:19;
then
k < x .. f
by NAT_1:13;
then
k + (x .. (Rev f)) < (len f) + 1
by A5, XREAL_1:6;
then
k + (x .. (Rev f)) <= len f
by NAT_1:13;
then A13:
k + (x .. (Rev f)) <= len (Rev f)
by FINSEQ_5:def 3;
A14:
1
<= (x .. f) - k
by A12, XREAL_1:19;
then
(x .. f) - k in NAT
by INT_1:5, XREAL_1:49;
then A15:
(((x .. f) - 1) - k) + 1
in dom (f | (Seg m))
by A7, A11, A14, A10, FINSEQ_3:25;
k <= k + (x .. (Rev f))
by NAT_1:11;
then
1
<= k + (x .. (Rev f))
by A9, XXREAL_0:2;
then A16:
k + (x .. (Rev f)) in dom (Rev f)
by A13, FINSEQ_3:25;
thus (Rev (f -| x)) . k =
(f -| x) . ((((x .. f) - 1) - k) + 1)
by A8, A11, FINSEQ_5:def 3
.=
f . (((len f) - (k + (x .. (Rev f)))) + 1)
by A5, A7, A15, FUNCT_1:47
.=
(Rev f) . (k + (x .. (Rev f)))
by A16, FINSEQ_5:def 3
;
verum end;
len (f -| x) =
(x .. f) - 1
by A3, FINSEQ_4:34
.=
(len f) - (x .. (Rev f))
by A5
.=
(len (Rev f)) - (x .. (Rev f))
by FINSEQ_5:def 3
;
hence
Rev (f -| x) = (Rev f) |-- x
by A4, A1, A6, FINSEQ_4:def 6; verum