the carrier of B c= the carrier of A by ALTCAT_2:def 11;
then reconsider CC = [:the carrier of B,the carrier of B:] as Subset of [:the carrier of A,the carrier of A:] by ZFMISC_1:119;
set OM = id [:the carrier of B,the carrier of B:];
id [:the carrier of B,the carrier of B:] = incl CC ;
then reconsider OM = id [:the carrier of B,the carrier of B:] as bifunction of the carrier of B,the carrier of A ;
set MM = id the Arrows of B;
id the Arrows of B is MSUnTrans of OM,the Arrows of B,the Arrows of A

proof

per cases ( [:the carrier of A,the carrier of A:] <> {} or [:the carrier of A,the carrier of A:] = {} ) ;
:: according to FUNCTOR0:def 4

case [:the carrier of A,the carrier of A:] <> {} ; :: thesis: ex I2' being non empty set ex B' being ManySortedSet of ex f' being Function of [:the carrier of B,the carrier of B:],I2' st
( OM = f' & the Arrows of A = B' & id the Arrows of B is ManySortedFunction of the Arrows of B,B' * f' )

then reconsider I2' = [:the carrier of A,the carrier of A:] as non empty set ;
reconsider B' = the Arrows of A as ManySortedSet of ;
reconsider f' = OM as Function of [:the carrier of B,the carrier of B:],I2' ;
take I2' ; :: thesis: ex B' being ManySortedSet of ex f' being Function of [:the carrier of B,the carrier of B:],I2' st
( OM = f' & the Arrows of A = B' & id the Arrows of B is ManySortedFunction of the Arrows of B,B' * f' )
take B' ; :: thesis: ex f' being Function of [:the carrier of B,the carrier of B:],I2' st
( OM = f' & the Arrows of A = B' & id the Arrows of B is ManySortedFunction of the Arrows of B,B' * f' )
take f' ; :: thesis: ( OM = f' & the Arrows of A = B' & id the Arrows of B is ManySortedFunction of the Arrows of B,B' * f' )
thus ( OM = f' & the Arrows of A = B' ) ; :: thesis: id the Arrows of B is ManySortedFunction of the Arrows of B,B' * f'
thus id the Arrows of B is ManySortedFunction of the Arrows of B,B' * f' :: thesis: verum

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in [:the carrier of B,the carrier of B:] or (id the Arrows of B) . i is Element of bool [:(the Arrows of B . i),((B' * f') . i):] )
assume A1: i in [:the carrier of B,the carrier of B:] ; :: thesis: (id the Arrows of B) . i is Element of bool [:(the Arrows of B . i),((B' * f') . i):]
then A2: (id the Arrows of B) . i is Function of (the Arrows of B . i),(the Arrows of B . i) by PBOOLE:def 18;
A3: the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
(B' * f') . i = B' . (f' . i) by A1, FUNCT_2:21
.= the Arrows of A . i by A1, FUNCT_1:35 ;
then the Arrows of B . i c= (B' * f') . i by A1, A3, ALTCAT_2:def 2;
hence (id the Arrows of B) . i is Element of bool [:(the Arrows of B . i),((B' * f') . i):] by A2, FUNCT_2:9; :: thesis: verum

end;

end;

case [:the carrier of A,the carrier of A:] = {} ; :: thesis: id the Arrows of B = [0] [:the carrier of B,the carrier of B:]

then A4: CC = {} ;
then id the Arrows of B = {} by PBOOLE:134;
hence id the Arrows of B = [0] [:the carrier of B,the carrier of B:] by A4; :: thesis: verum

end;

end;

end;

then reconsider MM = id the Arrows of B as MSUnTrans of OM,the Arrows of B,the Arrows of A ;
take FunctorStr(# OM,MM #) ; :: thesis: ( the ObjectMap of FunctorStr(# OM,MM #) = id [:the carrier of B,the carrier of B:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of B )
thus ( the ObjectMap of FunctorStr(# OM,MM #) = id [:the carrier of B,the carrier of B:] & the MorphMap of FunctorStr(# OM,MM #) = id the Arrows of B ) ; :: thesis: verum