let r be Real; :: thesis: r * <e1> = |[r,0,0]|
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) ;
then r * <e1> = |[(r * 1),(r * 0),(r * 0)]| by Lm1
.= |[r,0,0]| ;
hence r * <e1> = |[r,0,0]| ; :: thesis: verum