let r be 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>)
A1: ( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) ;
A2: ( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) ;
A3: ( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) ;
A4: (((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 A1, Lm1
.= (|[(r * (p . 1)),0,0]| + |[((r * (p . 2)) * 0),((r * (p . 2)) * 1),((r * (p . 2)) * 0)]|) + ((r * (p . 3)) * <e3>) by A2, Lm1
.= (|[(r * (p . 1)),0,0]| + |[0,(r * (p . 2)),0]|) + |[((r * (p . 3)) * 0),((r * (p . 3)) * 0),((r * (p . 3)) * 1)]| by A3, Lm1
.= (|[(r * (p . 1)),0,0]| + |[0,(r * (p . 2)),0]|) + |[0,0,(r * (p . 3))]| ;
A5: ( |[(r * (p . 1)),0,0]| . 1 = r * (p . 1) & |[(r * (p . 1)),0,0]| . 2 = 0 & |[(r * (p . 1)),0,0]| . 3 = 0 ) ;
A6: ( |[0,(r * (p . 2)),0]| . 1 = 0 & |[0,(r * (p . 2)),0]| . 2 = r * (p . 2) & |[0,(r * (p . 2)),0]| . 3 = 0 ) ;
A7: ( |[0,0,(r * (p . 3))]| . 1 = 0 & |[0,0,(r * (p . 3))]| . 2 = 0 & |[0,0,(r * (p . 3))]| . 3 = r * (p . 3) ) ;
A8: (((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 A4, A5, A6, Lm2
.= |[(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 ) ;
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 A7, A8, Lm2
.= |[(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 Lm1; :: thesis: verum