let x1, x2, x3, y1, y2, y3 be Element of REAL ; :: thesis: |[x1,x2,x3]| - |[y1,y2,y3]| = (((x1 - y1) * <e1> ) + ((x2 - y2) * <e2> )) + ((x3 - y3) * <e3> )
A1: |[y1,y2,y3]| . 1 = y1 by FINSEQ_1:62;
A2: |[y1,y2,y3]| . 2 = y2 by FINSEQ_1:62;
A3: |[y1,y2,y3]| . 3 = y3 by FINSEQ_1:62;
A4: (|[x1,x2,x3]| . 1) - (|[y1,y2,y3]| . 1) = x1 - y1 by A1, FINSEQ_1:62;
A5: (|[x1,x2,x3]| . 2) - (|[y1,y2,y3]| . 2) = x2 - y2 by A2, FINSEQ_1:62;
(|[x1,x2,x3]| . 3) - (|[y1,y2,y3]| . 3) = x3 - y3 by A3, FINSEQ_1:62;
hence |[x1,x2,x3]| - |[y1,y2,y3]| = (((x1 - y1) * <e1> ) + ((x2 - y2) * <e2> )) + ((x3 - y3) * <e3> ) by A4, A5, ThA18; :: thesis: verum