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:96;
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 3
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 B, the carrier of B:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
then reconsider I29 = [: the carrier of A, the carrier of A:] as non empty set ;
reconsider B9 = the Arrows of A as ManySortedSet of I29 ;
reconsider f9 = OM as Function of [: the carrier of B, the carrier of B:],I29 ;
take I29 ; :: thesis: ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
take B9 ; :: thesis: ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st
( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
take f9 ; :: thesis: ( OM = f9 & the Arrows of A = B9 & id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 )
thus ( OM = f9 & the Arrows of A = B9 ) ; :: thesis: id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9
thus id the Arrows of B is ManySortedFunction of the Arrows of B,B9 * f9 :: thesis: verum
proof
let i be object ; :: according to PBOOLE:def 15 :: 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),((B9 * f9) . 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),((B9 * f9) . 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 15;
A3: the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
(B9 * f9) . i = B9 . (f9 . i) by A1, FUNCT_2:15
.= the Arrows of A . i by A1, FUNCT_1:18 ;
then the Arrows of B . i c= (B9 * f9) . i by A1, A3, ALTCAT_2:def 2;
hence (id the Arrows of B) . i is Element of bool [:( the Arrows of B . i),((B9 * f9) . i):] by A2, FUNCT_2:7; :: thesis: verum
end;
end;
case [: the carrier of A, the carrier of A:] = {} ; :: thesis: id the Arrows of B = EmptyMS [: the carrier of B, the carrier of B:]
then CC = {} ;
hence id the Arrows of B = EmptyMS [: the carrier of B, the carrier of B:] ; :: 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