let n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)
let p be Element of D; :: thesis: for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)
let f be FinSequence of D; :: thesis: rng (Ins (f,n,p)) = {p} \/ (rng f)
thus rng (Ins (f,n,p)) = (rng ((f | n) ^ <*p*>)) \/ (rng (f /^ n)) by FINSEQ_1:31
.= ((rng (f | n)) \/ (rng <*p*>)) \/ (rng (f /^ n)) by FINSEQ_1:31
.= ((rng (f | n)) \/ (rng (f /^ n))) \/ (rng <*p*>) by XBOOLE_1:4
.= (rng ((f | n) ^ (f /^ n))) \/ (rng <*p*>) by FINSEQ_1:31
.= (rng <*p*>) \/ (rng f) by RFINSEQ:8
.= {p} \/ (rng f) by FINSEQ_1:38 ; :: thesis: verum