let x3, y3, x1, x2, y1, y2 be Real; :: thesis: |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3)
consider p1 being Point of (TOP-REAL 3) such that
A1: p1 = |[x1,x2,x3]| ;
A2: p1 `3 = x3 by A1, FINSEQ_1:45;
consider p2 being Point of (TOP-REAL 3) such that
A3: p2 = |[y1,y2,y3]| ;
A4: p2 `3 = y3 by A3, FINSEQ_1:45;
A5: ( p2 `1 = y1 & p2 `2 = y2 ) by A3, FINSEQ_1:45;
( p1 `1 = x1 & p1 `2 = x2 ) by A1, FINSEQ_1:45;
hence |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3) by A1, A2, A3, A5, A4, Th29; :: thesis: verum