Description: Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sadeq.a | |
|
sadeq.b | |
||
sadeq.n | |
||
Assertion | sadeq | |