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

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

p2 in rng (f /^ 1)

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

p2 in rng (f /^ 1)

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

assume that

A1: p2 in rng f and

A2: p2 .. f <> 1 ; :: thesis: p2 in rng (f /^ 1)

f = <*(f /. 1)*> ^ (f /^ 1) by A1, FINSEQ_5:29, RELAT_1:38;

then A3: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31;

assume not p2 in rng (f /^ 1) ; :: thesis: contradiction

then p2 in rng <*(f /. 1)*> by A1, A3, XBOOLE_0:def 3;

then p2 in {(f /. 1)} by FINSEQ_1:39;

then p2 = f /. 1 by TARSKI:def 1;

hence contradiction by A1, A2, Th43, RELAT_1:38; :: thesis: verum

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

p2 in rng (f /^ 1)

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

p2 in rng (f /^ 1)

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

assume that

A1: p2 in rng f and

A2: p2 .. f <> 1 ; :: thesis: p2 in rng (f /^ 1)

f = <*(f /. 1)*> ^ (f /^ 1) by A1, FINSEQ_5:29, RELAT_1:38;

then A3: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31;

assume not p2 in rng (f /^ 1) ; :: thesis: contradiction

then p2 in rng <*(f /. 1)*> by A1, A3, XBOOLE_0:def 3;

then p2 in {(f /. 1)} by FINSEQ_1:39;

then p2 = f /. 1 by TARSKI:def 1;

hence contradiction by A1, A2, Th43, RELAT_1:38; :: thesis: verum