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

per cases ( the carrier of S = {} or the carrier of S <> {} ) ;

suppose the carrier of S = {} ; :: thesis: a is Function

hence a is Function by SUBSET_1:def 2; :: thesis: verum

end;

suppose the carrier of S <> {} ; :: thesis: a is Function

hence a is Function by A1, FUNCT_1:def 19; :: thesis: verum

end;

end;