let r, x, y, z be 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))]|
.= |[(r * x),(r * y),(r * (|[x,y,z]| . 3))]|
.= |[(r * x),(r * y),(r * z)]| ;
hence r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]| ; :: thesis: verum