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 1,FUNCTOR0:def 12 :: thesis: the ObjectMap of (incl B) = [:f,f:]
thus the ObjectMap of (incl B) = id [: the carrier of B, the carrier of B:] by Def28
.= [:f,f:] by FUNCT_3:69 ; :: thesis: verum