let a be Real; :: thesis: for n being Nat holds a * (0* n) = 0* n
let n be Nat; :: thesis: a * (0* n) = 0* n
|.(a * (0* n)).| = |.a.| * |.(0* n).| by EUCLID:11
.= |.a.| * 0 by EUCLID:7
.= 0 ;
hence a * (0* n) = 0* n by EUCLID:8; :: thesis: verum