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;

.= (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

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)))

len (f -| x) =
(x .. f) - 1
by A3, FINSEQ_4:34
(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;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

.= (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