let x be set ; :: thesis: for f being FinSequence st f just_once_values x holds
Rev (f -| x) = (Rev f) |-- x
let f be FinSequence; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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; :: thesis: verum