let n be Nat; :: thesis: for x being real number holds x * (0.REAL n) = 0.REAL n
let x be real number ; :: thesis: x * (0.REAL n) = 0.REAL n
|.(x * (0* n)).| = (abs x) * |.(0* n).| by Th14
.= (abs x) * 0 by Th10
.= 0 ;
hence x * (0.REAL n) = 0.REAL n by Th11; :: thesis: verum