let x, y be Element of the_set_of_RealSequences ; :: thesis: ( ( for n being Element of NAT holds (seq_id x) . n = 0 ) & ( for n being Element of NAT holds (seq_id y) . n = 0 ) implies x = y )
assume that
A2: for n being Element of NAT holds (seq_id x) . n = 0 and
A3: for n being Element of NAT holds (seq_id y) . n = 0 ; :: thesis: x = y
A4: for s being set st s in NAT holds
(seq_id x) . s = (seq_id y) . s

proof

let s be set ; :: thesis: ( s in NAT implies (seq_id x) . s = (seq_id y) . s )
assume A5: s in NAT ; :: thesis: (seq_id x) . s = (seq_id y) . s
then (seq_id y) . s = 0 by A3;
hence (seq_id x) . s = (seq_id y) . s by A2, A5; :: thesis: verum

end;

x = seq_id x by Def2
.= seq_id y by A4, FUNCT_2:18 ;
hence x = y by Def2; :: thesis: verum