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