let A, B be non empty transitive with_units reflexive AltCatStr ; for F being feasible FunctorStr of A,B st F is bijective holds
(F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
set CCA = [:the carrier of A,the carrier of A:];
set CCB = [:the carrier of B,the carrier of B:];
let F be feasible FunctorStr of A,B; ( F is bijective implies (F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #) )
assume A1:
F is bijective
; (F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
A2:
F is injective
by A1, FUNCTOR0:def 36;
then
F is one-to-one
by FUNCTOR0:def 34;
then A3:
the ObjectMap of F is one-to-one
by FUNCTOR0:def 7;
A4:
F " is bijective
by A1, FUNCTOR0:36;
then
F " is surjective
by FUNCTOR0:def 36;
then A5:
F " is full
by FUNCTOR0:def 35;
F " is injective
by A4, FUNCTOR0:def 36;
then A6:
F " is faithful
by FUNCTOR0:def 34;
A7: the ObjectMap of (F " ) " =
(the ObjectMap of F " ) "
by A1, FUNCTOR0:def 39
.=
the ObjectMap of F
by A3, FUNCT_1:65
;
F is faithful
by A2, FUNCTOR0:def 34;
then A8:
the MorphMap of F is "1-1"
by FUNCTOR0:def 31;
A9:
F is surjective
by A1, FUNCTOR0:def 36;
then
F is onto
by FUNCTOR0:def 35;
then
the ObjectMap of F is onto
by FUNCTOR0:def 8;
then A10:
rng the ObjectMap of F = [:the carrier of B,the carrier of B:]
by FUNCT_2:def 3;
A11:
F is full
by A9, FUNCTOR0:def 35;
the MorphMap of ((F " ) " ) = the MorphMap of F
proof
A12:
ex
kk being
ManySortedFunction of the
Arrows of
B,the
Arrows of
A * the
ObjectMap of
(F " ) st
(
kk = the
MorphMap of
(F " ) &
kk is
"onto" )
by A5, FUNCTOR0:def 33;
A13:
ex
k being
ManySortedFunction of the
Arrows of
A,the
Arrows of
B * the
ObjectMap of
F st
(
k = the
MorphMap of
F &
k is
"onto" )
by A11, FUNCTOR0:def 33;
consider f being
ManySortedFunction of the
Arrows of
B,the
Arrows of
A * the
ObjectMap of
(F " ) such that A14:
f = the
MorphMap of
(F " )
and A15:
the
MorphMap of
((F " ) " ) = (f "" ) * (the ObjectMap of (F " ) " )
by A4, FUNCTOR0:def 39;
consider g being
ManySortedFunction of the
Arrows of
A,the
Arrows of
B * the
ObjectMap of
F such that A16:
g = the
MorphMap of
F
and A17:
the
MorphMap of
(F " ) = (g "" ) * (the ObjectMap of F " )
by A1, FUNCTOR0:def 39;
A18:
f is
"1-1"
by A6, A14, FUNCTOR0:def 31;
for
i being
set st
i in [:the carrier of A,the carrier of A:] holds
((f "" ) * (the ObjectMap of (F " ) " )) . i = the
MorphMap of
F . i
proof
A19:
the
ObjectMap of
F " is
Function of
[:the carrier of B,the carrier of B:],
[:the carrier of A,the carrier of A:]
by A3, A10, FUNCT_2:31;
let i be
set ;
( i in [:the carrier of A,the carrier of A:] implies ((f "" ) * (the ObjectMap of (F " ) " )) . i = the MorphMap of F . i )
assume A20:
i in [:the carrier of A,the carrier of A:]
;
((f "" ) * (the ObjectMap of (F " ) " )) . i = the MorphMap of F . i
then A21:
the
ObjectMap of
F . i in [:the carrier of B,the carrier of B:]
by FUNCT_2:7;
the
ObjectMap of
F " is
Function of
[:the carrier of B,the carrier of B:],
[:the carrier of A,the carrier of A:]
by A3, A10, FUNCT_2:31;
then A22:
(the ObjectMap of F " ) . (the ObjectMap of F . i) in [:the carrier of A,the carrier of A:]
by A21, FUNCT_2:7;
A23:
g . i is
one-to-one
by A8, A16, A20, MSUALG_3:1;
((f "" ) * (the ObjectMap of (F " ) " )) . i =
(f "" ) . (the ObjectMap of F . i)
by A7, A20, FUNCT_2:21
.=
(the MorphMap of (F " ) . (the ObjectMap of F . i)) "
by A14, A12, A18, A21, MSUALG_3:def 5
.=
((g "" ) . ((the ObjectMap of F " ) . (the ObjectMap of F . i))) "
by A17, A20, A19, FUNCT_2:7, FUNCT_2:21
.=
((g . ((the ObjectMap of F " ) . (the ObjectMap of F . i))) " ) "
by A8, A16, A13, A22, MSUALG_3:def 5
.=
((g . i) " ) "
by A3, A20, FUNCT_2:32
.=
the
MorphMap of
F . i
by A16, A23, FUNCT_1:65
;
hence
((f "" ) * (the ObjectMap of (F " ) " )) . i = the
MorphMap of
F . i
;
verum
end;
hence
the
MorphMap of
((F " ) " ) = the
MorphMap of
F
by A15, PBOOLE:3;
verum
end;
hence
(F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
by A4, A7, FUNCTOR0:def 39; verum