reconsider OM = id [:the carrier of A,the carrier of A:] as bifunction of the carrier of A,the carrier of A ;
set MM = id the Arrows of A;
id the Arrows of A is MSUnTrans of OM,the Arrows of A,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 I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [:the carrier of A,the carrier of A:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of A is ManySortedFunction of the Arrows of A,B9 * f9 )

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

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in [:the carrier of A,the carrier of A:] or (id the Arrows of A) . i is Element of bool [:(the Arrows of A . i),((A9 * f9) . i):] )
assume A1: i in [:the carrier of A,the carrier of A:] ; :: thesis: (id the Arrows of A) . i is Element of bool [:(the Arrows of A . i),((A9 * f9) . i):]
then (A9 * f9) . i = A9 . (f9 . i) by FUNCT_2:21
.= the Arrows of A . i by A1, FUNCT_1:35 ;
hence (id the Arrows of A) . i is Element of bool [:(the Arrows of A . i),((A9 * f9) . i):] by A1, PBOOLE:def 18; :: thesis: verum

end;

end;

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

hence id the Arrows of A = [[0]] [:the carrier of A,the carrier of A:] by PBOOLE:134; :: thesis: verum

end;

end;

end;

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