let S be RealNormSpace; :: thesis: for seq being sequence of S
for x being set holds
( x in rng seq iff ex n being Nat st x = seq . n )
let seq be sequence of S; :: thesis: for x being set holds
( x in rng seq iff ex n being Nat st x = seq . n )
let x be set ; :: thesis: ( x in rng seq iff ex n being Nat st x = seq . n )
thus ( x in rng seq implies ex n being Nat st x = seq . n ) :: thesis: ( ex n being Nat st x = seq . n implies x in rng seq )
proof
assume x in rng seq ; :: thesis: ex n being Nat st x = seq . n
then consider y being object such that
A1: y in dom seq and
A2: x = seq . y by FUNCT_1:def 3;
reconsider m = y as Nat by A1;
take m ; :: thesis: x = seq . m
thus x = seq . m by A2; :: thesis: verum
end;
given n being Nat such that A3: x = seq . n ; :: thesis: x in rng seq
n in NAT by ORDINAL1:def 12;
then n in dom seq by FUNCT_2:def 1;
hence x in rng seq by A3, FUNCT_1:def 3; :: thesis: verum