let p be Element of REAL 3; :: thesis: |(p,|[0,0,0]|)| = 0
set e = |[0,0,0]|;
( |[0,0,0]| . 1 = 0 & |[0,0,0]| . 2 = 0 & |[0,0,0]| . 3 = 0 ) ;
hence |(p,|[0,0,0]|)| = (((p . 1) * 0) + ((p . 2) * 0)) + ((p . 3) * 0) by Lm5
.= 0 ;
:: thesis: verum