let x1, y1, x2, y2 be real number ; :: thesis: |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]|
A1: ( |[x2,y2]| `1 = x2 & |[x2,y2]| `2 = y2 ) by FINSEQ_1:44;
( |[x1,y1]| `1 = x1 & |[x1,y1]| `2 = y1 ) by FINSEQ_1:44;
hence |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]| by A1, Th59; :: thesis: verum