0. (TOP-REAL 3) = 0* 3 by EUCLID:74
.= 3 |-> 0 by EUCLID:def 4
.= <*0 ,0 ,0 *> by FINSEQ_2:76 ;
hence 0. (TOP-REAL 3) = |[0 ,0 ,0 ]| ; :: thesis: verum