let x, y, z, r 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 Th49
.= |[(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