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