let seq, seq1 be Real_Sequence; :: thesis: ( seq1 = abs seq iff for n being Nat holds seq1 . n = |.(seq . n).| )

thus ( seq1 = abs seq implies for n being Nat holds seq1 . n = |.(seq . n).| ) by VALUED_1:18; :: thesis: ( ( for n being Nat holds seq1 . n = |.(seq . n).| ) implies seq1 = abs seq )

assume for n being Nat holds seq1 . n = |.(seq . n).| ; :: thesis: seq1 = abs seq

then A1: for n being object st n in dom seq1 holds

seq1 . n = |.(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

thus ( seq1 = abs seq implies for n being Nat holds seq1 . n = |.(seq . n).| ) by VALUED_1:18; :: thesis: ( ( for n being Nat holds seq1 . n = |.(seq . n).| ) implies seq1 = abs seq )

assume for n being Nat holds seq1 . n = |.(seq . n).| ; :: thesis: seq1 = abs seq

then A1: for n being object st n in dom seq1 holds

seq1 . n = |.(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