let S be 1-sorted ; :: thesis: ( the carrier of S is functional implies S is constituted-Functions )
assume A1: the carrier of S is functional ; :: thesis: S is constituted-Functions
let a be Element of S; :: according to MONOID_0:def 1 :: thesis: a is Function
thus a is Function by A1; :: thesis: verum