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

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