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
thus - (R1 - R2) = - (R1 + (- R2)) by FINSEQOP:89
.= (- R1) + (- (- R2)) by Th45
.= (- R1) + R2 ; :: thesis: verum