let p be Element of REAL 3; :: thesis: |(p,(0.REAL 3))| = 0
A1: 0.REAL 3 = |[0,0,0]| by FINSEQ_2:62;
then A2: (0.REAL 3) . 1 = 0 by FINSEQ_1:45;
A3: (0.REAL 3) . 2 = 0 by A1, FINSEQ_1:45;
(0.REAL 3) . 3 = 0 by A1, FINSEQ_1:45;
then |(p,(0.REAL 3))| = (((p . 1) * 0) + ((p . 2) * 0)) + ((p . 3) * 0) by A2, A3, Lm5;
hence |(p,(0.REAL 3))| = 0 ; :: thesis: verum