let A, B be Category; :: thesis: for F being Functor of A,B
for G being Functor of B,A st G * F ~= id A holds
F is faithful
let F be Functor of A,B; :: thesis: for G being Functor of B,A st G * F ~= id A holds
F is faithful
let G be Functor of B,A; :: thesis: ( G * F ~= id A implies F is faithful )
assume G * F ~= id A ; :: thesis: F is faithful
then A1: id A ~= G * F by NATTRA_1:31;
then A2: id A is_naturally_transformable_to G * F by NATTRA_1:def 11;
consider s being natural_transformation of id A,G * F such that
A3: s is invertible by A1, NATTRA_1:def 11;
thus F is faithful :: thesis: verum

proof

let a, a' be Object of A; :: according to CAT_1:def 24 :: thesis: ( Hom a,a' = {} or for b₁, b₂ being Morphism of a,a' holds
( not F . b₁ = F . b₂ or b₁ = b₂ ) )
assume A4: Hom a,a' <> {} ; :: thesis: for b₁, b₂ being Morphism of a,a' holds
( not F . b₁ = F . b₂ or b₁ = b₂ )
then A5: Hom ((id A) . a),((id A) . a') <> {} by CAT_1:126;
A6: Hom ((id A) . a'),((G * F) . a') <> {} by A2, Th30;
let f1, f2 be Morphism of a,a'; :: thesis: ( not F . f1 = F . f2 or f1 = f2 )
assume A7: F . f1 = F . f2 ; :: thesis: f1 = f2
A8: (G * F) . f1 = (G * F) . f1 by A4, NATTRA_1:def 1
.= G . (F . f2) by A7, FUNCT_2:21
.= (G * F) . f2 by FUNCT_2:21
.= (G * F) . f2 by A4, NATTRA_1:def 1 ;
s . a' is invertible by A3, NATTRA_1:def 10;
then A9: s . a' is monic by A6, CAT_1:73;
A10: (s . a') * ((id A) . f1) = ((G * F) . f1) * (s . a) by A2, A4, NATTRA_1:def 8
.= (s . a') * ((id A) . f2) by A2, A4, A8, NATTRA_1:def 8 ;
thus f1 = (id A) . f1 by A4, NATTRA_1:16
.= (id A) . f2 by A5, A6, A9, A10, CAT_1:60
.= f2 by A4, NATTRA_1:16 ; :: thesis: verum

end;