set OF = the ObjectMap of F;
F is injective by A1, Def36;
then F is one-to-one by Def34;
then A2: the ObjectMap of F is one-to-one by Def7;
F is surjective by A1, Def36;
then F is onto by Def35;
then the ObjectMap of F is onto by Def8;
then A3: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def 3;
then reconsider OM = the ObjectMap of F " as bifunction of the carrier of B, the carrier of A by A2, FUNCT_2:31;
reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by Def5;
( the Arrows of B * the ObjectMap of F) * OM = the Arrows of B * ( the ObjectMap of F * OM) by RELAT_1:55
.= the Arrows of B * (id [: the carrier of B, the carrier of B:]) by A2, A3, FUNCT_2:35
.= the Arrows of B by Th3 ;
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 Def5;
take G = FunctorStr(# OM,MM #); :: thesis: ( 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 " ; :: thesis: 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 ; :: thesis: ( 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 ") ) ; :: thesis: verum