let f be Element of the_set_of_RealSequences ; :: thesis: ( ( for n being Nat holds (seq_id f) . n = 0 ) implies f = Zeroseq )

set g = seq_id f;

assume A1: for n being Nat holds (seq_id f) . n = 0 ; :: thesis: f = Zeroseq

A2: dom (seq_id f) = NAT by FUNCT_2:def 1;

for z being object st z in dom (seq_id f) holds

(seq_id f) . z = 0 by A1;

hence f = Zeroseq by A2, FUNCOP_1:11; :: thesis: verum

set g = seq_id f;

assume A1: for n being Nat holds (seq_id f) . n = 0 ; :: thesis: f = Zeroseq

A2: dom (seq_id f) = NAT by FUNCT_2:def 1;

for z being object st z in dom (seq_id f) holds

(seq_id f) . z = 0 by A1;

hence f = Zeroseq by A2, FUNCOP_1:11; :: thesis: verum