theorem Th21: :: ANPROJ10:34

for a, r being Real holds multreal .: (((Seg 1) --> a),<*r*>) = <*(a * r)*>