set I = the set ;
set f = the multMagma-yielding ManySortedSet of the set ;
take the multMagma-yielding ManySortedSet of the set ; :: thesis: the multMagma-yielding ManySortedSet of the set is multMagma-yielding
thus the multMagma-yielding ManySortedSet of the set is multMagma-yielding ; :: thesis: verum