let r be Real; :: thesis: for seq being Real_Sequence holds
( r in rng seq iff - r in rng (- seq) )
let seq be Real_Sequence; :: thesis: ( r in rng seq iff - r in rng (- seq) )
thus ( r in rng seq implies - r in rng (- seq) ) :: thesis: ( - r in rng (- seq) implies r in rng seq )

proof

assume r in rng seq ; :: thesis: - r in rng (- seq)
then consider n being Element of NAT such that
A1: r = seq . n by FUNCT_2:113;
- r = (- seq) . n by A1, SEQ_1:10;
hence - r in rng (- seq) by VALUED_0:28; :: thesis: verum

end;

assume - r in rng (- seq) ; :: thesis: r in rng seq
then consider n being Element of NAT such that
A2: - r = (- seq) . n by FUNCT_2:113;
r = - ((- seq) . n) by A2;
then r = - (- (seq . n)) by SEQ_1:10;
hence r in rng seq by VALUED_0:28; :: thesis: verum