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*> = <*(addreal . (s1,s2))*> by FINSEQ_2:74
.= <*(r1 + r2)*> by BINOP_2:def 9 ;
hence <*r1*> + <*r2*> = <*(r1 + r2)*> ; :: thesis: verum