let x1, y1, z1, x2, y2, z2 be Real; :: thesis: |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 & |[x1,y1,z1]| `3 = z1 & |[x2,y2,z2]| `1 = x2 & |[x2,y2,z2]| `2 = y2 & |[x2,y2,z2]| `3 = z2 ) by FINSEQ_1:62;
hence |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]| by Th5; :: thesis: verum