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