n,m:
, f,g:(n
m
).
Thm* (
x:n, y:m. f(x,y) = g(x,y))
Thm*
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)
n:, f,g:(n).
Thm* (
i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n)| Theorem | Name |
| n,m:, f,g:(nm).
Thm* ( x:n, y:m. f(x,y) = g(x,y))
Thm*
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m) | [double_sum_functionality] |
| cites the following: | |
| n:, f,g:(n).
Thm* ( i:n. f(i) = g(i)) sum(f(x) | x < n) = sum(g(x) | x < n) | [sum_functionality] |