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