let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 = - seq2 iff for n being Element of NAT holds seq1 . n = - (seq2 . n) )
thus ( seq1 = - seq2 implies for n being Element of NAT holds seq1 . n = - (seq2 . n) ) by VALUED_1:8; :: thesis: ( ( for n being Element of NAT holds seq1 . n = - (seq2 . n) ) implies seq1 = - seq2 )
assume A1: for n being Element of NAT holds seq1 . n = - (seq2 . n) ; :: thesis: seq1 = - seq2
A2: dom seq1 = NAT by FUNCT_2:def 1
.= dom seq2 by FUNCT_2:def 1 ;
for n being set st n in dom seq1 holds
seq1 . n = - (seq2 . n) by A1;
hence seq1 = - seq2 by A2, VALUED_1:9; :: thesis: verum