let x be object ; :: thesis: for Y being non empty set

for f being sequence of Y holds

( x in rng f iff ex n being Nat st x = f . n )

let Y be non empty set ; :: thesis: for f being sequence of Y holds

( x in rng f iff ex n being Nat st x = f . n )

let f be sequence of Y; :: thesis: ( x in rng f iff ex n being Nat st x = f . n )

thus ( x in rng f implies ex n being Nat st x = f . n ) :: thesis: ( ex n being Nat st x = f . n implies x in rng f )

A4: n in NAT by ORDINAL1:def 12;

dom f = NAT by FUNCT_2:def 1;

hence x in rng f by A3, FUNCT_1:def 3, A4; :: thesis: verum

for f being sequence of Y holds

( x in rng f iff ex n being Nat st x = f . n )

let Y be non empty set ; :: thesis: for f being sequence of Y holds

( x in rng f iff ex n being Nat st x = f . n )

let f be sequence of Y; :: thesis: ( x in rng f iff ex n being Nat st x = f . n )

thus ( x in rng f implies ex n being Nat st x = f . n ) :: thesis: ( ex n being Nat st x = f . n implies x in rng f )

proof

given n being Nat such that A3:
x = f . n
; :: thesis: x in rng f
assume
x in rng f
; :: thesis: ex n being Nat st x = f . n

then consider y being object such that

A1: y in dom f and

A2: x = f . y by FUNCT_1:def 3;

reconsider m = y as Element of NAT by A1;

take m ; :: thesis: x = f . m

thus x = f . m by A2; :: thesis: verum

end;then consider y being object such that

A1: y in dom f and

A2: x = f . y by FUNCT_1:def 3;

reconsider m = y as Element of NAT by A1;

take m ; :: thesis: x = f . m

thus x = f . m by A2; :: thesis: verum

A4: n in NAT by ORDINAL1:def 12;

dom f = NAT by FUNCT_2:def 1;

hence x in rng f by A3, FUNCT_1:def 3, A4; :: thesis: verum