let x, y, z, r be Real; 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))]|
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)]|
; verum