let r be Element of REAL ; :: thesis: r * <e1> = |[r,0 ,0 ]|
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) by FINSEQ_1:62;
then r * <e1> = |[(r * 1),(r * 0 ),(r * 0 )]| by Lm3
.= |[r,0 ,0 ]| ;
hence r * <e1> = |[r,0 ,0 ]| ; :: thesis: verum