let D be non empty set ; :: thesis: for f being FinSequence of D
for p, q being Element of D st p in rng f & q in rng f & q .. f <= p .. f holds
(f -: p) :- q = (f :- q) -: p
let f be FinSequence of D; :: thesis: for p, q being Element of D st p in rng f & q in rng f & q .. f <= p .. f holds
(f -: p) :- q = (f :- q) -: p
let p, q be Element of D; :: thesis: ( p in rng f & q in rng f & q .. f <= p .. f implies (f -: p) :- q = (f :- q) -: p )
assume that
A1: p in rng f and
A2: q in rng f and
A3: q .. f <= p .. f ; :: thesis: (f -: p) :- q = (f :- q) -: p
A4: ( f -: p = f | (p .. f) & (f :- q) -: p = (f :- q) | (p .. (f :- q)) ) by FINSEQ_5:def 1;
consider i being Element of NAT such that
A5: i + 1 = q .. f and
A6: f :- q = f /^ i by A2, FINSEQ_5:49;
A7: i < p .. f by A3, A5, NAT_1:13;
then p .. f = i + (p .. (f /^ i)) by A1, FINSEQ_6:56;
then A8: p .. (f /^ i) = (p .. f) - i
.= (p .. f) -' i by A7, XREAL_1:233 ;
q in rng (f -: p) by A1, A2, A3, FINSEQ_5:46;
then A9: ex j being Element of NAT st
( j + 1 = q .. (f -: p) & (f -: p) :- q = (f -: p) /^ j ) by FINSEQ_5:49;
q .. (f -: p) = q .. f by A1, A2, A3, SPRECT_5:3;
hence (f -: p) :- q = (f :- q) -: p by A5, A6, A9, A4, A8, FINSEQ_5:80; :: thesis: verum