let r be Real; :: thesis: for seq1, seq2 being Real_Sequence holds

( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

thus ( seq1 = r (#) seq2 implies for n being Nat holds seq1 . n = r * (seq2 . n) ) by VALUED_1:6; :: thesis: ( ( for n being Nat holds seq1 . n = r * (seq2 . n) ) implies seq1 = r (#) seq2 )

assume for n being Nat holds seq1 . n = r * (seq2 . n) ; :: thesis: seq1 = r (#) seq2

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

seq1 . n = r * (seq2 . n) ;

dom seq1 = NAT by FUNCT_2:def 1

.= dom seq2 by FUNCT_2:def 1 ;

hence seq1 = r (#) seq2 by A1, VALUED_1:def 5; :: thesis: verum

( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

thus ( seq1 = r (#) seq2 implies for n being Nat holds seq1 . n = r * (seq2 . n) ) by VALUED_1:6; :: thesis: ( ( for n being Nat holds seq1 . n = r * (seq2 . n) ) implies seq1 = r (#) seq2 )

assume for n being Nat holds seq1 . n = r * (seq2 . n) ; :: thesis: seq1 = r (#) seq2

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

seq1 . n = r * (seq2 . n) ;

dom seq1 = NAT by FUNCT_2:def 1

.= dom seq2 by FUNCT_2:def 1 ;

hence seq1 = r (#) seq2 by A1, VALUED_1:def 5; :: thesis: verum