let r, x, y, z be Element of REAL ; :: thesis: r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]|
set p = |[x,y,z]|;
r * |[x,y,z]| = |[(r * (|[x,y,z]| . 1)),(r * (|[x,y,z]| . 2)),(r * (|[x,y,z]| . 3))]| by Lm1
.= |[(r * x),(r * (|[x,y,z]| . 2)),(r * (|[x,y,z]| . 3))]| by FINSEQ_1:45
.= |[(r * x),(r * y),(r * (|[x,y,z]| . 3))]| by FINSEQ_1:45
.= |[(r * x),(r * y),(r * z)]| by FINSEQ_1:45 ;
hence r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]| ; :: thesis: verum