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:] = {} )
;
FUNCTOR0:def 3case
[: the carrier of A, the carrier of A:] <> {}
;
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
;
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
;
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
;
( 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 )
;
id the Arrows of A is ManySortedFunction of the Arrows of A,A9 * f9thus
id the
Arrows of
A is
ManySortedFunction of the
Arrows of
A,
A9 * f9
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 #)
; ( 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 )
; verum