let x1, x2, x3, x4 be Real; :: thesis: - [*x1,x2,x3,x4*] = [*(- x1),(- x2),(- x3),(- x4)*]
[*x1,x2,x3,x4*] + [*(- x1),(- x2),(- x3),(- x4)*] = [*(x1 - x1),(x2 - x2),(x3 - x3),(x4 - x4)*] by QUATERNI:def 7
.= [*(In (0,REAL)),(In (0,REAL))*] by QUATERNI:91
.= 0 by ARYTM_0:def 5 ;
hence - [*x1,x2,x3,x4*] = [*(- x1),(- x2),(- x3),(- x4)*] by QUATERNI:def 8; :: thesis: verum