:: deftheorem defines Replace RVSUM_3:def 9 :
for f being Function
for i, j being Nat
for a, b being object holds Replace (f,i,j,a,b) = (f +* (i,a)) +* (j,b);