let r1, r2 be real number ; :: 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:88
.= <*(r1 - r2)*> by BINOP_2:def 10 ;
hence <*r1*> - <*r2*> = <*(r1 - r2)*> ; :: thesis: verum