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

end;