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