set f = the Function;
take X = 1-sorted(# { the Function} #); :: thesis: X is constituted-Functions
let a be Element of X; :: according to MONOID_0:def 1 :: thesis: a is Function
thus a is Function ; :: thesis: verum