let r be Element of REAL ; :: thesis: for p being Element of REAL 3 holds r * p = (((r * (p . 1)) * <e1> ) + ((r * (p . 2)) * <e2> )) + ((r * (p . 3)) * <e3> )
let p be Element of REAL 3; :: thesis: r * p = (((r * (p . 1)) * <e1> ) + ((r * (p . 2)) * <e2> )) + ((r * (p . 3)) * <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;
A5: (((r * (p . 1)) * <e1> ) + ((r * (p . 2)) * <e2> )) + ((r * (p . 3)) * <e3> ) = (|[((r * (p . 1)) * 1),((r * (p . 1)) * 0 ),((r * (p . 1)) * 0 )]| + ((r * (p . 2)) * <e2> )) + ((r * (p . 3)) * <e3> ) by A2, Lm3
.= (|[(r * (p . 1)),0 ,0 ]| + |[((r * (p . 2)) * 0 ),((r * (p . 2)) * 1),((r * (p . 2)) * 0 )]|) + ((r * (p . 3)) * <e3> ) by A3, Lm3
.= (|[(r * (p . 1)),0 ,0 ]| + |[0 ,(r * (p . 2)),0 ]|) + |[((r * (p . 3)) * 0 ),((r * (p . 3)) * 0 ),((r * (p . 3)) * 1)]| by A4, Lm3
.= (|[(r * (p . 1)),0 ,0 ]| + |[0 ,(r * (p . 2)),0 ]|) + |[0 ,0 ,(r * (p . 3))]| ;
A6: ( |[(r * (p . 1)),0 ,0 ]| . 1 = r * (p . 1) & |[(r * (p . 1)),0 ,0 ]| . 2 = 0 & |[(r * (p . 1)),0 ,0 ]| . 3 = 0 ) by FINSEQ_1:62;
A7: ( |[0 ,(r * (p . 2)),0 ]| . 1 = 0 & |[0 ,(r * (p . 2)),0 ]| . 2 = r * (p . 2) & |[0 ,(r * (p . 2)),0 ]| . 3 = 0 ) by FINSEQ_1:62;
A8: ( |[0 ,0 ,(r * (p . 3))]| . 1 = 0 & |[0 ,0 ,(r * (p . 3))]| . 2 = 0 & |[0 ,0 ,(r * (p . 3))]| . 3 = r * (p . 3) ) by FINSEQ_1:62;
A9: (((r * (p . 1)) * <e1> ) + ((r * (p . 2)) * <e2> )) + ((r * (p . 3)) * <e3> ) = |[((r * (p . 1)) + 0 ),(0 + (r * (p . 2))),(0 + 0 )]| + |[0 ,0 ,(r * (p . 3))]| by A5, A6, A7, Lm4
.= |[(r * (p . 1)),(r * (p . 2)),0 ]| + |[0 ,0 ,(r * (p . 3))]| ;
( |[(r * (p . 1)),(r * (p . 2)),0 ]| . 1 = r * (p . 1) & |[(r * (p . 1)),(r * (p . 2)),0 ]| . 2 = r * (p . 2) & |[(r * (p . 1)),(r * (p . 2)),0 ]| . 3 = 0 ) by FINSEQ_1:62;
then (((r * (p . 1)) * <e1> ) + ((r * (p . 2)) * <e2> )) + ((r * (p . 3)) * <e3> ) = |[((r * (p . 1)) + 0 ),((r * (p . 2)) + 0 ),(0 + (r * (p . 3)))]| by A8, A9, Lm4
.= |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]| ;
hence r * p = (((r * (p . 1)) * <e1> ) + ((r * (p . 2)) * <e2> )) + ((r * (p . 3)) * <e3> ) by Lm3; :: thesis: verum