let x, x1, y1, z1 be Real; :: thesis: x * |[x1,y1,z1]| = |[(x * x1),(x * y1),(x * z1)]|
A1: |[x1,y1,z1]| `3 = z1 by FINSEQ_1:45;
( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 ) by FINSEQ_1:45;
hence x * |[x1,y1,z1]| = |[(x * x1),(x * y1),(x * z1)]| by A1, Th7; :: thesis: verum