let A, B, C be non empty transitive with_units reflexive AltCatStr ; for G being feasible FunctorStr over A,B
for F being feasible FunctorStr over B,C
for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over 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 over A,B; for F being feasible FunctorStr over B,C
for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over 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 over B,C; for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over 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 over B,A; for FI being feasible FunctorStr over 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 over 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 4;
A5:
MF is "1-1"
by A1, Th5;
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, Th2, Th5;
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, Th2, Th5;
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 4;
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 4;
A6:
MG is "1-1"
by A2, Th5;
F is surjective
by A1;
then
F is full
;
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" )
;
F is injective
by A1;
then
F is one-to-one
;
then A8:
the ObjectMap of F is one-to-one
;
A9:
G is surjective
by A2;
then
G is onto
;
then A10:
the ObjectMap of G is onto
;
G is full
by A9;
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" )
;
G is injective
by A2;
then
G is one-to-one
;
then A12:
the ObjectMap of G is one-to-one
;
A13:
F * G is bijective
by A1, A2, Th12;
then
F * G is surjective
;
then
F * G is full
;
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" )
;
A15:
MFG is "1-1"
by A13, Th5;
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 38;
A19:
rng the
ObjectMap of
G = [: the carrier of B, the carrier of B:]
by A10, FUNCT_2:def 3;
for
i being
object 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 38;
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 38, PARTFUN1:def 2;
A22:
OG * (OG ") = id [: the carrier of B, the carrier of B:]
by A12, A19, FUNCT_2:29;
A23:
OFG " =
( the ObjectMap of F * OG) "
by FUNCTOR0:def 36
.=
(OG ") * ( the ObjectMap of F ")
by A8, A12, FUNCT_1:44
;
let i be
object ;
( 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:15
.=
((MF . ((OG * OGI) . (OFI . i))) * (MG . ((OFG ") . i))) "
by A24, FUNCT_2:5, FUNCT_2:15
.=
((MF . (((id [: the carrier of B, the carrier of B:]) * OFI) . i)) * (MG . ((OFG ") . i))) "
by A24, A22, FUNCT_2:15
.=
((MF . (( the ObjectMap of F ") . i)) * (MG . ((OGI * OFI) . i))) "
by A23, FUNCT_2:17
;
OFG " is
Function of
[: the carrier of C, the carrier of C:],
[: the carrier of A, the carrier of A:]
by A13, Th2, Th5;
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:5, PARTFUN1:def 2;
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, Th2, Th5;
then A28:
( the ObjectMap of (F * G) ") . i in [: the carrier of A, the carrier of A:]
by A24, FUNCT_2:5;
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:13
.=
(MFG . (( the ObjectMap of (F * G) ") . i)) "
by A14, A15, A28, MSUALG_3:def 4
.=
(((MF * OG) ** MG) . ((OFG ") . i)) "
by FUNCTOR0:def 36
.=
(((MF * OG) . ((OFG ") . i)) * (MG . ((OFG ") . i))) "
by A26, PBOOLE:def 19
.=
((MF . (OG . (((OG ") * ( the ObjectMap of F ")) . i))) * (MG . ((OFG ") . i))) "
by A24, A27, A23, FUNCT_2:5, FUNCT_2:15
;
A30:
OFI . i in [: the carrier of B, the carrier of B:]
by A24, FUNCT_2:5;
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:5;
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:15
.=
((MG . (OGI . (OFI . i))) ") * ((MF . (OFI . i)) ")
by A33, A31, FUNCT_1:44
.=
((MG "") . (OGI . (OFI . i))) * ((MF . (( the ObjectMap of F ") . i)) ")
by A11, A6, A32, MSUALG_3:def 4
.=
(((MG "") * OGI) . (OFI . i)) * ((MF . (( the ObjectMap of F ") . i)) ")
by A24, FUNCT_2:5, FUNCT_2:15
.=
((((MG "") * OGI) * OFI) . i) * ((MF . (OFI . i)) ")
by A24, FUNCT_2:15
.=
((((MG "") * OGI) * OFI) . i) * ((MF "") . (OFI . i))
by A5, A7, A30, MSUALG_3:def 4
.=
((((MG "") * OGI) * OFI) . i) * (((MF "") * OFI) . i)
by A24, FUNCT_2:15
;
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 19;
verum
end;
then the
MorphMap of
((F * G) ") =
( the MorphMap of GI * the ObjectMap of FI) ** the
MorphMap of
FI
by A3, A4, A18
.=
the
MorphMap of
(GI * FI)
by FUNCTOR0:def 36
;
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 38
.=
( the ObjectMap of F * the ObjectMap of G) "
by FUNCTOR0:def 36
.=
( the ObjectMap of G ") * ( the ObjectMap of F ")
by A8, A12, FUNCT_1:44
.=
the ObjectMap of GI * ( the ObjectMap of F ")
by A2, A3, FUNCTOR0:def 38
.=
the ObjectMap of GI * the ObjectMap of FI
by A1, A4, FUNCTOR0:def 38
.=
the ObjectMap of (GI * FI)
by FUNCTOR0:def 36
;
hence
(F * G) " = GI * FI
by A16; verum