let x1, y1, z1 be Real; :: thesis: - |[x1,y1,z1]| = |[(- x1),(- y1),(- z1)]|
A1: |[x1,y1,z1]| `3 = z1 by FINSEQ_1:62;
( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 ) by FINSEQ_1:62;
hence - |[x1,y1,z1]| = |[(- x1),(- y1),(- z1)]| by A1, Th10; :: thesis: verum