reconsider b = the carrier of B as Subset of A by ALTCAT_2:def 11;
incl b = id b ;
then reconsider f = id the carrier of B as Function of the carrier of B,the carrier of A ;
take f ; :: according to FUNCTOR0:def 2,FUNCTOR0:def 13 :: thesis: the ObjectMap of (incl B) = [:f,f:]
thus the ObjectMap of (incl B) = id [:the carrier of B,the carrier of B:] by Def29
.= [:f,f:] by FUNCT_3:90 ; :: thesis: verum