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