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