let A, B, C be non empty transitive with_units reflexive AltCatStr ; for G being feasible FunctorStr of A,B
for F being feasible FunctorStr of B,C
for GI being feasible FunctorStr of B,A
for FI being feasible FunctorStr of C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let G be feasible FunctorStr of A,B; for F being feasible FunctorStr of B,C
for GI being feasible FunctorStr of B,A
for FI being feasible FunctorStr of C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let F be feasible FunctorStr of B,C; for GI being feasible FunctorStr of B,A
for FI being feasible FunctorStr of C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let GI be feasible FunctorStr of B,A; for FI being feasible FunctorStr of C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
let FI be feasible FunctorStr of C,B; ( F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F " implies (F * G) " = GI * FI )
assume that
A1:
F is bijective
and
A2:
G is bijective
and
A3:
FunctorStr(# the ObjectMap of GI,the MorphMap of GI #) = G "
and
A4:
FunctorStr(# the ObjectMap of FI,the MorphMap of FI #) = F "
; (F * G) " = GI * FI
reconsider MF = the MorphMap of F as ManySortedFunction of the Arrows of B,the Arrows of C * the ObjectMap of F by FUNCTOR0:def 5;
A5:
MF is "1-1"
by A1, Th6;
set OG = the ObjectMap of G;
set CB = [:the carrier of B,the carrier of B:];
set CA = [:the carrier of A,the carrier of A:];
reconsider OGI = the ObjectMap of G " as Function of [:the carrier of B,the carrier of B:],[:the carrier of A,the carrier of A:] by A2, Th3, Th6;
set CC = [:the carrier of C,the carrier of C:];
set OF = the ObjectMap of F;
reconsider OFI = the ObjectMap of F " as Function of [:the carrier of C,the carrier of C:],[:the carrier of B,the carrier of B:] by A1, Th3, Th6;
reconsider MFG = the MorphMap of (F * G) as ManySortedFunction of the Arrows of A,the Arrows of C * the ObjectMap of (F * G) by FUNCTOR0:def 5;
reconsider OG = the ObjectMap of G as Function of [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:] ;
reconsider OFG = the ObjectMap of (F * G) as Function of [:the carrier of A,the carrier of A:],[:the carrier of C,the carrier of C:] ;
reconsider MG = the MorphMap of G as ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of G by FUNCTOR0:def 5;
A6:
MG is "1-1"
by A2, Th6;
F is surjective
by A1, FUNCTOR0:def 36;
then
F is full
by FUNCTOR0:def 35;
then A7:
ex mf being ManySortedFunction of the Arrows of B,the Arrows of C * the ObjectMap of F st
( mf = the MorphMap of F & mf is "onto" )
by FUNCTOR0:def 33;
F is injective
by A1, FUNCTOR0:def 36;
then
F is one-to-one
by FUNCTOR0:def 34;
then A8:
the ObjectMap of F is one-to-one
by FUNCTOR0:def 7;
A9:
G is surjective
by A2, FUNCTOR0:def 36;
then
G is onto
by FUNCTOR0:def 35;
then A10:
the ObjectMap of G is onto
by FUNCTOR0:def 8;
G is full
by A9, FUNCTOR0:def 35;
then A11:
ex mg being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of G st
( mg = the MorphMap of G & mg is "onto" )
by FUNCTOR0:def 33;
G is injective
by A2, FUNCTOR0:def 36;
then
G is one-to-one
by FUNCTOR0:def 34;
then A12:
the ObjectMap of G is one-to-one
by FUNCTOR0:def 7;
A13:
F * G is bijective
by A1, A2, Th13;
then
F * G is surjective
by FUNCTOR0:def 36;
then
F * G is full
by FUNCTOR0:def 35;
then A14:
ex mfg being ManySortedFunction of the Arrows of A,the Arrows of C * the ObjectMap of (F * G) st
( mfg = the MorphMap of (F * G) & mfg is "onto" )
by FUNCTOR0:def 33;
A15:
MFG is "1-1"
by A13, Th6;
A16:
the MorphMap of ((F * G) " ) = the MorphMap of (GI * FI)
proof
consider f being
ManySortedFunction of the
Arrows of
A,the
Arrows of
C * the
ObjectMap of
(F * G) such that A17:
f = the
MorphMap of
(F * G)
and A18:
the
MorphMap of
((F * G) " ) = (f "" ) * (the ObjectMap of (F * G) " )
by A13, FUNCTOR0:def 39;
A19:
rng the
ObjectMap of
G = [:the carrier of B,the carrier of B:]
by A10, FUNCT_2:def 3;
for
i being
set st
i in [:the carrier of C,the carrier of C:] holds
((f "" ) * (the ObjectMap of (F * G) " )) . i = ((the MorphMap of (G " ) * the ObjectMap of (F " )) ** the MorphMap of (F " )) . i
proof
A20:
( ex
x1 being
ManySortedFunction of the
Arrows of
B,the
Arrows of
C * the
ObjectMap of
F st
(
x1 = the
MorphMap of
F & the
MorphMap of
(F " ) = (x1 "" ) * (the ObjectMap of F " ) ) & ex
x1 being
ManySortedFunction of the
Arrows of
A,the
Arrows of
B * the
ObjectMap of
G st
(
x1 = the
MorphMap of
G & the
MorphMap of
(G " ) = (x1 "" ) * (the ObjectMap of G " ) ) )
by A1, A2, FUNCTOR0:def 39;
A21:
( the
ObjectMap of
F " = the
ObjectMap of
(F " ) &
dom ((((MG "" ) * OGI) * OFI) ** ((MF "" ) * OFI)) = [:the carrier of C,the carrier of C:] )
by A1, FUNCTOR0:def 39, PARTFUN1:def 4;
A22:
OG * (OG " ) = id [:the carrier of B,the carrier of B:]
by A12, A19, FUNCT_2:35;
A23:
OFG " =
(the ObjectMap of F * OG) "
by FUNCTOR0:def 37
.=
(OG " ) * (the ObjectMap of F " )
by A8, A12, FUNCT_1:66
;
let i be
set ;
( i in [:the carrier of C,the carrier of C:] implies ((f "" ) * (the ObjectMap of (F * G) " )) . i = ((the MorphMap of (G " ) * the ObjectMap of (F " )) ** the MorphMap of (F " )) . i )
assume A24:
i in [:the carrier of C,the carrier of C:]
;
((f "" ) * (the ObjectMap of (F * G) " )) . i = ((the MorphMap of (G " ) * the ObjectMap of (F " )) ** the MorphMap of (F " )) . i
A25:
((MF . (OG . (((OG " ) * (the ObjectMap of F " )) . i))) * (MG . ((OFG " ) . i))) " =
((MF . (OG . (OGI . (OFI . i)))) * (MG . ((OFG " ) . i))) "
by A24, FUNCT_2:21
.=
((MF . ((OG * OGI) . (OFI . i))) * (MG . ((OFG " ) . i))) "
by A24, FUNCT_2:7, FUNCT_2:21
.=
((MF . (((id [:the carrier of B,the carrier of B:]) * OFI) . i)) * (MG . ((OFG " ) . i))) "
by A24, A22, FUNCT_2:21
.=
((MF . ((the ObjectMap of F " ) . i)) * (MG . ((OGI * OFI) . i))) "
by A23, FUNCT_2:23
;
OFG " is
Function of
[:the carrier of C,the carrier of C:],
[:the carrier of A,the carrier of A:]
by A13, Th3, Th6;
then A26:
(
dom ((MF * OG) ** MG) = [:the carrier of A,the carrier of A:] &
(OFG " ) . i in [:the carrier of A,the carrier of A:] )
by A24, FUNCT_2:7, PARTFUN1:def 4;
A27:
the
ObjectMap of
(F * G) " is
Function of
[:the carrier of C,the carrier of C:],
[:the carrier of A,the carrier of A:]
by A13, Th3, Th6;
then A28:
(the ObjectMap of (F * G) " ) . i in [:the carrier of A,the carrier of A:]
by A24, FUNCT_2:7;
i in dom (the ObjectMap of (F * G) " )
by A24, A27, FUNCT_2:def 1;
then A29:
((f "" ) * (the ObjectMap of (F * G) " )) . i =
(MFG "" ) . ((the ObjectMap of (F * G) " ) . i)
by A17, FUNCT_1:23
.=
(MFG . ((the ObjectMap of (F * G) " ) . i)) "
by A14, A15, A28, MSUALG_3:def 5
.=
(((MF * OG) ** MG) . ((OFG " ) . i)) "
by FUNCTOR0:def 37
.=
(((MF * OG) . ((OFG " ) . i)) * (MG . ((OFG " ) . i))) "
by A26, PBOOLE:def 24
.=
((MF . (OG . (((OG " ) * (the ObjectMap of F " )) . i))) * (MG . ((OFG " ) . i))) "
by A24, A27, A23, FUNCT_2:7, FUNCT_2:21
;
A30:
OFI . i in [:the carrier of B,the carrier of B:]
by A24, FUNCT_2:7;
then A31:
MF . (OFI . i) is
one-to-one
by A5, MSUALG_3:1;
A32:
OGI . (OFI . i) in [:the carrier of A,the carrier of A:]
by A30, FUNCT_2:7;
then A33:
MG . (OGI . (OFI . i)) is
one-to-one
by A6, MSUALG_3:1;
((MF . ((the ObjectMap of F " ) . i)) * (MG . ((OGI * OFI) . i))) " =
((MF . ((the ObjectMap of F " ) . i)) * (MG . (OGI . (OFI . i)))) "
by A24, FUNCT_2:21
.=
((MG . (OGI . (OFI . i))) " ) * ((MF . (OFI . i)) " )
by A33, A31, FUNCT_1:66
.=
((MG "" ) . (OGI . (OFI . i))) * ((MF . ((the ObjectMap of F " ) . i)) " )
by A11, A6, A32, MSUALG_3:def 5
.=
(((MG "" ) * OGI) . (OFI . i)) * ((MF . ((the ObjectMap of F " ) . i)) " )
by A24, FUNCT_2:7, FUNCT_2:21
.=
((((MG "" ) * OGI) * OFI) . i) * ((MF . (OFI . i)) " )
by A24, FUNCT_2:21
.=
((((MG "" ) * OGI) * OFI) . i) * ((MF "" ) . (OFI . i))
by A5, A7, A30, MSUALG_3:def 5
.=
((((MG "" ) * OGI) * OFI) . i) * (((MF "" ) * OFI) . i)
by A24, FUNCT_2:21
;
hence
((f "" ) * (the ObjectMap of (F * G) " )) . i = ((the MorphMap of (G " ) * the ObjectMap of (F " )) ** the MorphMap of (F " )) . i
by A20, A24, A21, A29, A25, PBOOLE:def 24;
verum
end;
then the
MorphMap of
((F * G) " ) =
(the MorphMap of GI * the ObjectMap of FI) ** the
MorphMap of
FI
by A3, A4, A18, PBOOLE:3
.=
the
MorphMap of
(GI * FI)
by FUNCTOR0:def 37
;
hence
the
MorphMap of
((F * G) " ) = the
MorphMap of
(GI * FI)
;
verum
end;
the ObjectMap of ((F * G) " ) =
the ObjectMap of (F * G) "
by A13, FUNCTOR0:def 39
.=
(the ObjectMap of F * the ObjectMap of G) "
by FUNCTOR0:def 37
.=
(the ObjectMap of G " ) * (the ObjectMap of F " )
by A8, A12, FUNCT_1:66
.=
the ObjectMap of GI * (the ObjectMap of F " )
by A2, A3, FUNCTOR0:def 39
.=
the ObjectMap of GI * the ObjectMap of FI
by A1, A4, FUNCTOR0:def 39
.=
the ObjectMap of (GI * FI)
by FUNCTOR0:def 37
;
hence
(F * G) " = GI * FI
by A16; verum