let r1, r2 be Real; :: thesis: <*r1*> - <*r2*> = <*(r1 - r2)*>
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;
<*s1*> - <*s2*> = <*(diffreal . (s1,s2))*> by FINSEQ_2:74
.= <*(r1 - r2)*> by BINOP_2:def 10 ;
hence <*r1*> - <*r2*> = <*(r1 - r2)*> ; :: thesis: verum