let k be Nat; :: thesis: for Y being non empty set

for f being sequence of Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }

let Y be non empty set ; :: thesis: for f being sequence of Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }

let f be sequence of Y; :: thesis: rng (f ^\ k) = { (f . n) where n is Nat : k <= n }

reconsider f1 = f ^\ k as sequence of Y ;

rng f1 = { (f . m) where m is Nat : k <= m }

for f being sequence of Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }

let Y be non empty set ; :: thesis: for f being sequence of Y holds rng (f ^\ k) = { (f . n) where n is Nat : k <= n }

let f be sequence of Y; :: thesis: rng (f ^\ k) = { (f . n) where n is Nat : k <= n }

reconsider f1 = f ^\ k as sequence of Y ;

rng f1 = { (f . m) where m is Nat : k <= m }

proof

hence
rng (f ^\ k) = { (f . n) where n is Nat : k <= n }
; :: thesis: verum
set Z = { (f . m) where m is Nat : k <= m } ;

A1: dom f1 = NAT by FUNCT_2:def 1;

A2: rng f1 c= { (f . m) where m is Nat : k <= m }

end;A1: dom f1 = NAT by FUNCT_2:def 1;

A2: rng f1 c= { (f . m) where m is Nat : k <= m }

proof

{ (f . m) where m is Nat : k <= m } c= rng f1
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f1 or y in { (f . m) where m is Nat : k <= m } )

assume y in rng f1 ; :: thesis: y in { (f . m) where m is Nat : k <= m }

then consider m1 being object such that

A3: m1 in NAT and

A4: y = f1 . m1 by A1, FUNCT_1:def 3;

reconsider m1 = m1 as Element of NAT by A3;

y = f . (k + m1) by A4, NAT_1:def 3;

hence y in { (f . m) where m is Nat : k <= m } by Th1; :: thesis: verum

end;assume y in rng f1 ; :: thesis: y in { (f . m) where m is Nat : k <= m }

then consider m1 being object such that

A3: m1 in NAT and

A4: y = f1 . m1 by A1, FUNCT_1:def 3;

reconsider m1 = m1 as Element of NAT by A3;

y = f . (k + m1) by A4, NAT_1:def 3;

hence y in { (f . m) where m is Nat : k <= m } by Th1; :: thesis: verum

proof

hence
rng f1 = { (f . m) where m is Nat : k <= m }
by A2, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . m) where m is Nat : k <= m } or x in rng f1 )

assume x in { (f . m) where m is Nat : k <= m } ; :: thesis: x in rng f1

then consider k1 being Nat such that

A5: x = f . k1 and

A6: k <= k1 ;

consider k2 being Nat such that

A7: k1 = k + k2 by A6, NAT_1:10;

( k2 in NAT & x = f1 . k2 ) by A5, A7, NAT_1:def 3, ORDINAL1:def 12;

hence x in rng f1 by FUNCT_2:4; :: thesis: verum

end;assume x in { (f . m) where m is Nat : k <= m } ; :: thesis: x in rng f1

then consider k1 being Nat such that

A5: x = f . k1 and

A6: k <= k1 ;

consider k2 being Nat such that

A7: k1 = k + k2 by A6, NAT_1:10;

( k2 in NAT & x = f1 . k2 ) by A5, A7, NAT_1:def 3, ORDINAL1:def 12;

hence x in rng f1 by FUNCT_2:4; :: thesis: verum