let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace f,i,p)
let f be FinSequence of D; :: thesis: for p being Element of D
for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace f,i,p)
let p be Element of D; :: thesis: for i being Nat st 1 <= i & i <= len f holds
p in rng (Replace f,i,p)
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies p in rng (Replace f,i,p) )
A1: rng (((f | (i -' 1)) ^ <*p*>) ^ (f /^ i)) = rng ((f | (i -' 1)) ^ (<*p*> ^ (f /^ i))) by FINSEQ_1:45
.= (rng (f | (i -' 1))) \/ (rng (<*p*> ^ (f /^ i))) by FINSEQ_1:44
.= (rng (f | (i -' 1))) \/ ((rng <*p*>) \/ (rng (f /^ i))) by FINSEQ_1:44 ;
p in {p} by TARSKI:def 1;
then A2: p in rng <*p*> by FINSEQ_1:56;
assume ( 1 <= i & i <= len f ) ; :: thesis: p in rng (Replace f,i,p)
then rng (Replace f,i,p) = (rng (f | (i -' 1))) \/ ((rng <*p*>) \/ (rng (f /^ i))) by A1, Def1
.= (rng <*p*>) \/ ((rng (f /^ i)) \/ (rng (f | (i -' 1)))) by XBOOLE_1:4 ;
hence p in rng (Replace f,i,p) by A2, XBOOLE_0:def 3; :: thesis: verum