let Y be non empty set ; :: thesis: for f being sequence of Y holds rng f = { (f . k) where k is Nat : 0 <= k }
let f be sequence of Y; :: thesis: rng f = { (f . k) where k is Nat : 0 <= k }
set Z = { (f . k) where k is Nat : 0 <= k } ;
A1: dom f = NAT by FUNCT_2:def 1;
A2: rng f c= { (f . k) where k is Nat : 0 <= k }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { (f . k) where k is Nat : 0 <= k } )
assume y in rng f ; :: thesis: y in { (f . k) where k is Nat : 0 <= k }
then consider n being object such that
A3: n in NAT and
A4: y = f . n by A1, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A3;
0 <= n by NAT_1:2;
hence y in { (f . k) where k is Nat : 0 <= k } by A4; :: thesis: verum

end;

{ (f . k) where k is Nat : 0 <= k } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . k) where k is Nat : 0 <= k } or x in rng f )
assume x in { (f . k) where k is Nat : 0 <= k } ; :: thesis: x in rng f
then consider n1 being Nat such that
A5: ( x = f . n1 & 0 <= n1 ) ;
n1 in NAT by ORDINAL1:def 12;
hence x in rng f by FUNCT_2:4, A5; :: thesis: verum

end;

hence rng f = { (f . k) where k is Nat : 0 <= k } by A2, XBOOLE_0:def 10; :: thesis: verum