let p1, p2 be Element of REAL 3; :: thesis: |((- p1),p2)| = - |(p1,p2)|
A2: - p1 = |[(- (p1 . 1)),(- (p1 . 2)),(- (p1 . 3))]| by Th39;
A3: (- p1) . 1 = - (p1 . 1) by A2, FINSEQ_1:62;
A4: (- p1) . 2 = - (p1 . 2) by A2, FINSEQ_1:62;
A5: (- p1) . 3 = - (p1 . 3) by A2, FINSEQ_1:62;
A6: |(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3)) by Lm8;
|((- p1),p2)| = (((- (p1 . 1)) * (p2 . 1)) + ((- (p1 . 2)) * (p2 . 2))) + ((- (p1 . 3)) * (p2 . 3)) by A3, A4, A5, Lm8;
hence |((- p1),p2)| = - |(p1,p2)| by A6; :: thesis: verum