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