thus REAL 0 = {(<*> REAL )} by FINSEQ_2:112
.= {(0. (TOP-REAL 0 ))} ; :: thesis: verum