let seq1, seq be Real_Sequence; :: thesis: ( seq1 = abs seq iff for n being Element of NAT holds seq1 . n = abs (seq . n) )
thus ( seq1 = abs seq implies for n being Element of NAT holds seq1 . n = abs (seq . n) ) by VALUED_1:18; :: thesis: ( ( for n being Element of NAT holds seq1 . n = abs (seq . n) ) implies seq1 = abs seq )
assume for n being Element of NAT holds seq1 . n = abs (seq . n) ; :: thesis: seq1 = abs seq
then A1: for n being set st n in dom seq1 holds
seq1 . n = abs (seq . n) ;
dom seq1 = NAT by FUNCT_2:def 1
.= dom seq by FUNCT_2:def 1 ;
hence seq1 = abs seq by A1, VALUED_1:def 11; :: thesis: verum