A2: F is one-to-one by A1;
rng F = the carrier' of B by A1;
then reconsider G = F " as Function of the carrier' of B, the carrier' of A by A2, FUNCT_2:25;
A3: dom F = the carrier' of A by FUNCT_2:def 1;
A4: Obj F is one-to-one by A2, Th7;
G is Functor of B,A

proof

thus for c being Object of B ex d being Object of A st G . (id c) = id d :: according to ISOCAT_1:def 1 :: thesis: ( ( for f being Morphism of B holds
( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
G . (g (*) f) = (G . g) (*) (G . f) ) )

proof

let b be Object of B; :: thesis: ex d being Object of A st G . (id b) = id d
consider a being Object of A such that
A5: F . a = b by A1, Th6;
take a ; :: thesis: G . (id b) = id a
thus G . (id b) = G . (F . (id a)) by A5, CAT_1:71
.= id a by A2, A3, FUNCT_1:34 ; :: thesis: verum

end;

thus for f being Morphism of B holds
( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) :: thesis: for f, g being Morphism of B st dom g = cod f holds
G . (g (*) f) = (G . g) (*) (G . f)

proof

let f be Morphism of B; :: thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) )
consider g being Morphism of A such that
A6: f = F . g by A1, Th5;
thus G . (id (dom f)) = G . (id (F . (dom g))) by A6, CAT_1:72
.= G . (F . (id (dom g))) by CAT_1:71
.= id (dom g) by A2, A3, FUNCT_1:34
.= id (dom (G . f)) by A2, A3, A6, FUNCT_1:34 ; :: thesis: G . (id (cod f)) = id (cod (G . f))
thus G . (id (cod f)) = G . (id (F . (cod g))) by A6, CAT_1:72
.= G . (F . (id (cod g))) by CAT_1:71
.= id (cod g) by A2, A3, FUNCT_1:34
.= id (cod (G . f)) by A2, A3, A6, FUNCT_1:34 ; :: thesis: verum

end;

let f, g be Morphism of B; :: thesis: ( dom g = cod f implies G . (g (*) f) = (G . g) (*) (G . f) )
A7: dom (Obj F) = the carrier of A by FUNCT_2:def 1;
assume A8: dom g = cod f ; :: thesis: G . (g (*) f) = (G . g) (*) (G . f)
consider f9 being Morphism of A such that
A9: f = F . f9 by A1, Th5;
consider g9 being Morphism of A such that
A10: g = F . g9 by A1, Th5;
(Obj F) . (dom g9) = F . (dom g9)
.= cod f by A10, A8, CAT_1:72
.= F . (cod f9) by A9, CAT_1:72
.= (Obj F) . (cod f9) ;
then dom g9 = cod f9 by A4, A7;
hence G . (g (*) f) = G . (F . (g9 (*) f9)) by A9, A10, CAT_1:64
.= g9 (*) f9 by A2, A3, FUNCT_1:34
.= g9 (*) (G . f) by A2, A3, A9, FUNCT_1:34
.= (G . g) (*) (G . f) by A2, A3, A10, FUNCT_1:34 ;
:: thesis: verum

end;

hence F " is Functor of B,A ; :: thesis: verum