let n be Nat; :: thesis: for D being non empty set
for f being FinSequence of D holds rng (f /^ n) c= rng f
let D be non empty set ; :: thesis: for f being FinSequence of D holds rng (f /^ n) c= rng f
let f be FinSequence of D; :: thesis: rng (f /^ n) c= rng f
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in rng (f /^ n) or p in rng f )
assume p in rng (f /^ n) ; :: thesis: p in rng f
then consider j being Element of NAT such that
A1: j in dom (f /^ n) and
A2: (f /^ n) /. j = p by PARTFUN2:2;
j + n in dom f by A1, Th26;
then f /. (j + n) in rng f by PARTFUN2:2;
hence p in rng f by A1, A2, Th27; :: thesis: verum