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 ;
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 ;
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 ;
k in dom (f -| x) by ;
then k <= (x .. f) - 1 by ;
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 ;
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 ;
then (x .. f) - k in NAT by ;
then A15: (((x .. f) - 1) - k) + 1 in dom (f | (Seg m)) by ;
k <= k + (x .. (Rev f)) by NAT_1:11;
then 1 <= k + (x .. (Rev f)) by ;
then A16: k + (x .. (Rev f)) in dom (Rev f) by ;
thus (Rev (f -| x)) . k = (f -| x) . ((((x .. f) - 1) - k) + 1) by
.= f . (((len f) - (k + (x .. (Rev f)))) + 1) by
.= (Rev f) . (k + (x .. (Rev f))) by ; :: thesis: verum
end;
len (f -| x) = (x .. f) - 1 by
.= (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 ; :: thesis: verum