thus a = a * ((1. F) ")
.= a / (1. F) by ALGSTR_0:def 43 ; :: thesis: verum