let x, y, z be Real; :: thesis: |[0,0,0]| <X> |[x,y,z]| = 0. (TOP-REAL 3)
|[0,0,0]| <X> |[x,y,z]| = |[((0 * z) - (0 * y)),((0 * x) - (0 * z)),((0 * y) - (0 * x))]| by Th15
.= |[(0 * (z - y)),(0 * (x - z)),(0 * (y - x))]|
.= 0 * |[(z - y),(x - z),(y - x)]| by Th8 ;
hence |[0,0,0]| <X> |[x,y,z]| = 0. (TOP-REAL 3) by RLVECT_1:10; :: thesis: verum