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 #); :: 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