let T be non empty RelStr ; :: thesis: id the carrier of T in MonFuncs (T,T)
reconsider IT = id T as Function of the carrier of T, the carrier of T ;
reconsider IT9 = IT as Function of T,T ;
( id T is monotone & IT9 in Funcs ( the carrier of T, the carrier of T) ) by FUNCT_2:9;
hence id the carrier of T in MonFuncs (T,T) by Def6; :: thesis: verum