Description: X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fmuldfeq.1 | |
|
fmuldfeq.2 | |
||
fmuldfeq.3 | |
||
fmuldfeq.4 | |
||
fmuldfeq.5 | |
||
fmuldfeq.6 | |
||
fmuldfeq.7 | |
||
fmuldfeq.8 | |
||
fmuldfeq.9 | |
||
fmuldfeq.10 | |
||
fmuldfeq.11 | |
||
Assertion | fmuldfeq | |