let r, x, y, z be Element of REAL ; :: thesis: r * |[x,y,z]| = (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>)
A2: ( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) by FINSEQ_1:62;
A3: ( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) by FINSEQ_1:62;
A4: ( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) by FINSEQ_1:62;
set p = |[x,y,z]|;
A6: (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>) = (|[((r * x) * 1),((r * x) * 0),((r * x) * 0)]| + ((r * y) * <e2>)) + ((r * z) * <e3>) by A2, Lm3
.= (|[(r * x),0,0]| + |[((r * y) * 0),((r * y) * 1),((r * y) * 0)]|) + ((r * z) * <e3>) by A3, Lm3
.= (|[(r * x),0,0]| + |[0,(r * y),0]|) + |[((r * z) * 0),((r * z) * 0),((r * z) * 1)]| by A4, Lm3
.= (|[(r * x),0,0]| + |[0,(r * y),0]|) + |[0,0,(r * z)]| ;
A7: ( |[(r * x),0,0]| . 1 = r * x & |[(r * x),0,0]| . 2 = 0 & |[(r * x),0,0]| . 3 = 0 ) by FINSEQ_1:62;
A8: ( |[0,(r * y),0]| . 1 = 0 & |[0,(r * y),0]| . 2 = r * y & |[0,(r * y),0]| . 3 = 0 ) by FINSEQ_1:62;
A9: ( |[0,0,(r * z)]| . 1 = 0 & |[0,0,(r * z)]| . 2 = 0 & |[0,0,(r * z)]| . 3 = r * z ) by FINSEQ_1:62;
A10: (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>) = |[((r * x) + 0),((r * y) + 0),(0 + 0)]| + |[0,0,(r * z)]| by A6, A7, A8, Lm4
.= |[(r * x),(r * y),0]| + |[0,0,(r * z)]| ;
( |[(r * x),(r * y),0]| . 1 = r * x & |[(r * x),(r * y),0]| . 2 = r * y & |[(r * x),(r * y),0]| . 3 = 0 ) by FINSEQ_1:62;
then (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>) = |[((r * x) + 0),((r * y) + 0),(0 + (r * z))]| by A9, A10, Lm4
.= |[(r * x),(r * y),(r * z)]| ;
hence r * |[x,y,z]| = (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>) by LmA8; :: thesis: verum