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