let i be Nat; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds - (R1 + R2) = (- R1) + (- R2)
let R1, R2 be Element of i -tuples_on REAL ; :: thesis: - (R1 + R2) = (- R1) + (- R2)
(R1 + R2) + ((- R1) + (- R2)) = ((R1 + R2) + (- R1)) + (- R2) by FINSEQOP:29
.= (R2 + (R1 + (- R1))) + (- R2) by Th32
.= (R2 + (i |-> 0 )) + (- R2) by Th22, Th23, BINOP_2:2, FINSEQOP:77
.= R2 + (- R2) by BINOP_2:2, FINSEQOP:57
.= i |-> 0 by Th22, Th23, BINOP_2:2, FINSEQOP:77 ;
hence - (R1 + R2) = (- R1) + (- R2) by Th22, Th23, BINOP_2:2, FINSEQOP:78; :: thesis: verum