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 }

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

{ (f . k) where k is Nat : 0 <= k } c= rng f
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;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

proof

hence
rng f = { (f . k) where k is Nat : 0 <= k }
by A2, XBOOLE_0:def 10; :: thesis: verum
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;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