Theorem Function.End.mul_def

Modification history