let x, y be Element of the_set_of_ComplexSequences ; :: thesis: ( ( for n being Element of NAT holds (seq_id x) . n = 0c ) & ( for n being Element of NAT holds (seq_id y) . n = 0c ) implies x = y )
assume that
A3: for n being Element of NAT holds (seq_id x) . n = 0c and
A4: for n being Element of NAT holds (seq_id y) . n = 0c ; :: thesis: x = y
A5: for s being Element of NAT holds (seq_id x) . s = (seq_id y) . s

proof

let s be Element of NAT ; :: thesis: (seq_id x) . s = (seq_id y) . s
(seq_id y) . s = 0c by A4;
hence (seq_id x) . s = (seq_id y) . s by A3; :: thesis: verum

end;

x = seq_id x by Def2
.= seq_id y by A5, FUNCT_2:63 ;
hence x = y by Def2; :: thesis: verum