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:28;
then A2: id A is_naturally_transformable_to G * F ;
consider s being natural_transformation of id A,G * F such that
A3: s is invertible by A1;
thus F is faithful :: thesis: verum

proof

let a, a9 be Object of A; :: according to CAT_1:def 27 :: 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:84;
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, CAT_3:def 10
.= G . (F . f2) by A6, FUNCT_2:15
.= (G * F) . f2 by FUNCT_2:15
.= (G * F) /. f2 by A4, CAT_3:def 10 ;
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 ;
s . a9 is invertible by A3;
then A9: s . a9 is monic by CAT_1:43;
thus f1 = (id A) /. f1 by A4, NATTRA_1:16
.= (id A) /. f2 by A5, A9, A8
.= f2 by A4, NATTRA_1:16 ; :: thesis: verum

end;