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)).| = (abs a) * |.(0* n).| by EUCLID:14
.= (abs a) * 0 by EUCLID:10
.= 0 ;
hence a * (0* n) = 0* n by EUCLID:11; :: thesis: verum