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