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 & p .. f <= q .. f holds
q .. (f :- p) = ((q .. f) - (p .. f)) + 1
let f be FinSequence of D; :: thesis: for p, q being Element of D st p in rng f & q in rng f & p .. f <= q .. f holds
q .. (f :- p) = ((q .. f) - (p .. f)) + 1
let p, q be Element of D; :: thesis: ( p in rng f & q in rng f & p .. f <= q .. f implies q .. (f :- p) = ((q .. f) - (p .. f)) + 1 )
assume that
A1: p in rng f and
A2: q in rng f and
A3: p .. f <= q .. f ; :: thesis: q .. (f :- p) = ((q .. f) - (p .. f)) + 1
A4: f = (f | (p .. f)) ^ (f /^ (p .. f)) by RFINSEQ:21;

per cases ( p .. f = q .. f or p .. f < q .. f ) by A3, XXREAL_0:1;

suppose p .. f = q .. f ; :: thesis: q .. (f :- p) = ((q .. f) - (p .. f)) + 1

then p = q by A1, A2, FINSEQ_5:10;
hence q .. (f :- p) = ((q .. f) - (p .. f)) + 1 by FINSEQ_6:84; :: thesis: verum

end;

suppose A5: p .. f < q .. f ; :: thesis: q .. (f :- p) = ((q .. f) - (p .. f)) + 1

then A6: not q in rng (f | (p .. f)) by Th1;
p .. f <= len f by A1, FINSEQ_4:31;
then A7: len (f | (p .. f)) = p .. f by FINSEQ_1:80;
q in (rng (f | (p .. f))) \/ (rng (f /^ (p .. f))) by A2, A4, FINSEQ_1:44;
then A8: q in rng (f /^ (p .. f)) by A6, XBOOLE_0:def 3;
then q in (rng (f /^ (p .. f))) \ (rng (f | (p .. f))) by A6, XBOOLE_0:def 5;
then A9: q .. f = (p .. f) + (q .. (f /^ (p .. f))) by A4, A7, FINSEQ_6:9;
not q in {p} by A5, TARSKI:def 1;
then not q in rng <*p*> by FINSEQ_1:55;
then A10: q in (rng (f /^ (p .. f))) \ (rng <*p*>) by A8, XBOOLE_0:def 5;
f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def 2;
hence q .. (f :- p) = (len <*p*>) + (q .. (f /^ (p .. f))) by A10, FINSEQ_6:9
.= ((q .. f) - (p .. f)) + 1 by A9, FINSEQ_1:56 ;
:: thesis: verum

end;

end;