theorem :: MONOID_0:80

for S being 1-sorted st the carrier of S is functional holds
S is constituted-Functions ;