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
ISOCAT_1:def 1 ( ( 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) ) )
thus
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 f be
Morphism of
B;
( 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
;
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
;
verum
end;
let f,
g be
Morphism of
B;
( 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
;
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
;
verum
end;
hence
F " is Functor of B,A
; verum