let x1, y1 be Real; :: thesis: - |[x1,y1]| = |[(- x1),(- y1)]|
( |[x1,y1]| `1 = x1 & |[x1,y1]| `2 = y1 ) by FINSEQ_1:44;
hence - |[x1,y1]| = |[(- x1),(- y1)]| by Th31; :: thesis: verum