let n be Nat; :: thesis: for f being FinSequence holds rng (f /^ n) c= rng f
let f be FinSequence; :: 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 object such that
A1: j in dom (f /^ n) and
A2: (f /^ n) . j = p by FUNCT_1:def 3;
reconsider jj = j as Nat by A1;
jj + n in dom f by A1, Th26;
then f . (jj + n) in rng f by FUNCT_1:def 3;
hence p in rng f by A1, A2, Th27; :: thesis: verum