let n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (Ins (f,n,p))
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds p in rng (Ins (f,n,p))
let p be Element of D; :: thesis: for f being FinSequence of D holds p in rng (Ins (f,n,p))
let f be FinSequence of D; :: thesis: p in rng (Ins (f,n,p))
p in {p} by TARSKI:def 1;
then p in {p} \/ (rng f) by XBOOLE_0:def 3;
hence p in rng (Ins (f,n,p)) by Th70; :: thesis: verum