theorem
proved
actionDerivativeProductRuleNearZero_of_factorDifferentiability
show as:
actionDerivativeProductRuleNearZero_of_factorDifferentiability