consider I being set , f being multMagma-yielding ManySortedSet of I;
take f ; :: thesis: f is multMagma-yielding
thus f is multMagma-yielding ; :: thesis: verum