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

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

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

assume that

A1: p in rng f and

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

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

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

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

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

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

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

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

assume that

A1: p in rng f and

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

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

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

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