let T be non empty RelStr ; :: thesis: id the carrier of T in MonFuncs T,T
A1: id T is monotone by Lm4;
reconsider IT = id T as Function of the carrier of T,the carrier of T ;
reconsider IT' = IT as Function of T,T ;
IT' in Funcs the carrier of T,the carrier of T by FUNCT_2:12;
hence id the carrier of T in MonFuncs T,T by A1, Def6; :: thesis: verum