let N be Element of NAT ; :: thesis: for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)
let r be Real; :: thesis: for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)
let seq1, seq2 be Real_Sequence of N; :: thesis: r * (seq1 + seq2) = (r * seq1) + (r * seq2)

now

let n be Element of NAT ; :: thesis: (r * (seq1 + seq2)) . n = ((r * seq1) + (r * seq2)) . n
thus (r * (seq1 + seq2)) . n = r * ((seq1 + seq2) . n) by Def3
.= r * ((seq1 . n) + (seq2 . n)) by Def2
.= (r * (seq1 . n)) + (r * (seq2 . n)) by EUCLID:36
.= ((r * seq1) . n) + (r * (seq2 . n)) by Def3
.= ((r * seq1) . n) + ((r * seq2) . n) by Def3
.= ((r * seq1) + (r * seq2)) . n by Def2 ; :: thesis: verum

end;

hence r * (seq1 + seq2) = (r * seq1) + (r * seq2) by FUNCT_2:113; :: thesis: verum