let x, x1, y1 be Real; :: thesis: x * |[x1,y1]| = |[(x * x1),(x * y1)]|
( |[x1,y1]| `1 = x1 & |[x1,y1]| `2 = y1 ) by FINSEQ_1:44;
hence x * |[x1,y1]| = |[(x * x1),(x * y1)]| by Th29; :: thesis: verum