let p be Element of REAL 3; :: thesis: for r being Real holds r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|
let r be Real; :: thesis: r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]|
A1: (r * p) . 1 = r * (p . 1) by RVSUM_1:44;
A2: (r * p) . 2 = r * (p . 2) by RVSUM_1:44;
(r * p) . 3 = r * (p . 3) by RVSUM_1:44;
hence r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]| by A1, A2, Th1; :: thesis: verum