let i be Nat; :: thesis: for r1, r2 being real number holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)
let r1, r2 be real number ; :: thesis: (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;
(i |-> s1) + (i |-> s2) = i |-> (addreal . s1,s2) by FINSEQOP:18
.= i |-> (r1 + r2) by BINOP_2:def 9 ;
hence (i |-> r1) + (i |-> r2) = i |-> (r1 + r2) ; :: thesis: verum