let f be Element of the_set_of_ComplexSequences ; :: thesis: ( ( for n being Nat holds (seq_id f) . n = 0 ) implies f = CZeroseq )
set g = seq_id f;
assume A1: for n being Nat holds (seq_id f) . n = 0 ; :: thesis: f = CZeroseq
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 = CZeroseq by A2, FUNCOP_1:11; :: thesis: verum