- = (D[x · x \sup (1+m)]) by _.
- = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]) by _.
- = (x \sup (1+m) + x · (costante (1+m) · x \sup m)) by _.
-clear H.
- = (x \sup (1+m) + costante (1+m) · x \sup (1+m)) by _.
- = (x \sup (1+m) · (costante (2 + m))) by _
+ = (D[x · x \sup (1+m)]).
+ = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]).
+ = (x \sup (1+m) + x · (costante (1+m) · x \sup m)).
+ = (x \sup (1+m) + costante (1+m) · x \sup (1+m)).
+ = ((2+m) · x \sup (1+m)) by Fmult_one_f Fmult_commutative
+ Fmult_Fplus_distr assoc_plus plus_n_SO costante_sum