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