take <* the non empty multMagma *> ; :: thesis: ( not <* the non empty multMagma *> is empty & <* the non empty multMagma *> is FinSequence-like & <* the non empty multMagma *> is multMagma-yielding )
thus ( not <* the non empty multMagma *> is empty & <* the non empty multMagma *> is FinSequence-like & <* the non empty multMagma *> is multMagma-yielding ) ; :: thesis: verum