let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) -: p = (f -: p) /^ 1

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) -: p = (f -: p) /^ 1

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f <> 1 implies (f /^ 1) -: p = (f -: p) /^ 1 )

assume that

A1: p in rng f and

A2: p .. f <> 1 ; :: thesis: (f /^ 1) -: p = (f -: p) /^ 1

p .. f >= 1 by A1, FINSEQ_4:21;

then p .. f > 1 by A2, XXREAL_0:1;

hence (f /^ 1) -: p = (f -: p) /^ 1 by A1, Th59; :: thesis: verum

for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) -: p = (f -: p) /^ 1

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f <> 1 holds

(f /^ 1) -: p = (f -: p) /^ 1

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f <> 1 implies (f /^ 1) -: p = (f -: p) /^ 1 )

assume that

A1: p in rng f and

A2: p .. f <> 1 ; :: thesis: (f /^ 1) -: p = (f -: p) /^ 1

p .. f >= 1 by A1, FINSEQ_4:21;

then p .. f > 1 by A2, XXREAL_0:1;

hence (f /^ 1) -: p = (f -: p) /^ 1 by A1, Th59; :: thesis: verum