let p be Element of REAL 3; :: thesis: |(p,(0.REAL 3))| = 0
0.REAL 3 = |[0,0,0]| by FINSEQ_2:62;
hence |(p,(0.REAL 3))| = 0 by Th13; :: thesis: verum