let x1, x2, x3, y1, y2, y3 be Element of REAL ; :: thesis: |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3)
set p1 = |[x1,x2,x3]|;
A2: ( |[x1,x2,x3]| . 1 = x1 & |[x1,x2,x3]| . 2 = x2 & |[x1,x2,x3]| . 3 = x3 ) by FINSEQ_1:62;
set p2 = |[y1,y2,y3]|;
( |[y1,y2,y3]| . 1 = y1 & |[y1,y2,y3]| . 2 = y2 & |[y1,y2,y3]| . 3 = y3 ) by FINSEQ_1:62;
hence |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3) by A2, LmB30; :: thesis: verum