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

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