let N be 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)
thus r * (seq1 - seq2) = (r * seq1) + (r * (- seq2)) by Th12
.= (r * seq1) + (r * ((- 1) * seq2)) by Th11
.= (r * seq1) + (((- 1) * r) * seq2) by Th13
.= (r * seq1) + ((- 1) * (r * seq2)) by Th13
.= (r * seq1) - (r * seq2) by Th11 ; :: thesis: verum