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 Th73; :: thesis: verum