A2: F is one-to-one by A1, CAT_1:def 22;
then A3: Obj F is one-to-one by Th12;
A4: rng F = the carrier' of B by A1, CAT_1:def 22;
A5: dom F = the carrier' of A by FUNCT_2:def 1;
reconsider G = F " as Function of the carrier' of B,the carrier' of A by A2, A4, FUNCT_2:31;
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
A6: F . a = b by A1, Th11;
take a ; :: thesis: G . (id b) = id a
thus G . (id b) = G . (F . (id a)) by A6, CAT_1:108
.= id a by A2, A5, FUNCT_1:56 ; :: 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
A7: f = F . g by A1, Th10;
thus G . (id (dom f)) = G . (id (F . (dom g))) by A7, CAT_1:109
.= G . (F . (id (dom g))) by CAT_1:108
.= id (dom g) by A2, A5, FUNCT_1:56
.= id (dom (G . f)) by A2, A5, A7, FUNCT_1:56 ; :: thesis: G . (id (cod f)) = id (cod (G . f))
thus G . (id (cod f)) = G . (id (F . (cod g))) by A7, CAT_1:109
.= G . (F . (id (cod g))) by CAT_1:108
.= id (cod g) by A2, A5, FUNCT_1:56
.= id (cod (G . f)) by A2, A5, A7, FUNCT_1:56 ; :: thesis: verum

end;

let f, g be Morphism of B; :: thesis: ( dom g = cod f implies G . (g * f) = (G . g) * (G . f) )
consider f' being Morphism of A such that
A8: f = F . f' by A1, Th10;
consider g' being Morphism of A such that
A9: g = F . g' by A1, Th10;
A10: dom (Obj F) = the carrier of A by FUNCT_2:def 1;
assume A11: dom g = cod f ; :: thesis: G . (g * f) = (G . g) * (G . f)
(Obj F) . (dom g') = F . (dom g')
.= cod f by A9, A11, CAT_1:109
.= F . (cod f') by A8, CAT_1:109
.= (Obj F) . (cod f') ;
then dom g' = cod f' by A3, A10, FUNCT_1:def 8;
hence G . (g * f) = G . (F . (g' * f')) by A8, A9, CAT_1:99
.= g' * f' by A2, A5, FUNCT_1:56
.= g' * (G . f) by A2, A5, A8, FUNCT_1:56
.= (G . g) * (G . f) by A2, A5, A9, FUNCT_1:56 ;
:: thesis: verum

end;

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