set OF = the ObjectMap of F;
F is injective
by A1;
then
F is one-to-one
;
then A2:
the ObjectMap of F is one-to-one
;
F is surjective
by A1;
then
F is onto
;
then
the ObjectMap of F is onto
;
then A3:
rng the ObjectMap of F = [: the carrier of B, the carrier of B:]
;
then reconsider OM = the ObjectMap of F " as bifunction of the carrier of B, the carrier of A by A2, FUNCT_2:25;
reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by Def4;
( the Arrows of B * the ObjectMap of F) * OM =
the Arrows of B * ( the ObjectMap of F * OM)
by RELAT_1:36
.=
the Arrows of B * (id [: the carrier of B, the carrier of B:])
by A2, A3, FUNCT_2:29
.=
the Arrows of B
by Th2
;
then
(f "") * OM is ManySortedFunction of the Arrows of B, the Arrows of A * OM
by ALTCAT_2:5;
then reconsider MM = (f "") * OM as MSUnTrans of OM, the Arrows of B, the Arrows of A by Def4;
take G = FunctorStr(# OM,MM #); ( the ObjectMap of G = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") ) )
thus
the ObjectMap of G = the ObjectMap of F "
; ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") )
take
f
; ( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") )
thus
( f = the MorphMap of F & the MorphMap of G = (f "") * ( the ObjectMap of F ") )
; verum