let C, D be Category; :: thesis: for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C holds rng (hom T,c,c9) = Hom (T . c),(T . c9) )
let T be Functor of C,D; :: thesis: ( T is full iff for c, c9 being Object of C holds rng (hom T,c,c9) = Hom (T . c),(T . c9) )
thus ( T is full implies for c, c9 being Object of C holds rng (hom T,c,c9) = Hom (T . c),(T . c9) ) :: thesis: ( ( for c, c9 being Object of C holds rng (hom T,c,c9) = Hom (T . c),(T . c9) ) implies T is full )

proof

assume A1: T is full ; :: thesis: for c, c9 being Object of C holds rng (hom T,c,c9) = Hom (T . c),(T . c9)
let c, c9 be Object of C; :: thesis: rng (hom T,c,c9) = Hom (T . c),(T . c9)

now

assume A2: Hom (T . c),(T . c9) <> {} ; :: thesis: rng (hom T,c,c9) = Hom (T . c),(T . c9)
for g being set holds
( g in rng (hom T,c,c9) iff g in Hom (T . c),(T . c9) )

proof

let g be set ; :: thesis: ( g in rng (hom T,c,c9) iff g in Hom (T . c),(T . c9) )
thus ( g in rng (hom T,c,c9) implies g in Hom (T . c),(T . c9) ) :: thesis: ( g in Hom (T . c),(T . c9) implies g in rng (hom T,c,c9) )

proof

assume g in rng (hom T,c,c9) ; :: thesis: g in Hom (T . c),(T . c9)
then consider f being set such that
A3: f in dom (hom T,c,c9) and
A4: (hom T,c,c9) . f = g by FUNCT_1:def 5;
f in Hom c,c9 by A2, A3, FUNCT_2:def 1;
hence g in Hom (T . c),(T . c9) by A2, A4, FUNCT_2:7; :: thesis: verum

end;

assume g in Hom (T . c),(T . c9) ; :: thesis: g in rng (hom T,c,c9)
then g is Morphism of T . c,T . c9 by Def7;
then consider f being Morphism of c,c9 such that
A5: g = T . f by A1, A2, Def23;
A6: Hom c,c9 <> {} by A1, A2, Def23;
then f in Hom c,c9 by Def7;
then (hom T,c,c9) . f in rng (hom T,c,c9) by A2, FUNCT_2:6;
hence g in rng (hom T,c,c9) by A5, A6, Th131; :: thesis: verum

end;

hence rng (hom T,c,c9) = Hom (T . c),(T . c9) by TARSKI:2; :: thesis: verum

end;

hence rng (hom T,c,c9) = Hom (T . c),(T . c9) ; :: thesis: verum

end;

assume A7: for c, c9 being Object of C holds rng (hom T,c,c9) = Hom (T . c),(T . c9) ; :: thesis: T is full
let c, c9 be Object of C; :: according to CAT_1:def 23 :: thesis: ( Hom (T . c),(T . c9) <> {} implies for g being Morphism of T . c,T . c9 holds
( Hom c,c9 <> {} & ex f being Morphism of c,c9 st g = T . f ) )
assume A8: Hom (T . c),(T . c9) <> {} ; :: thesis: for g being Morphism of T . c,T . c9 holds
( Hom c,c9 <> {} & ex f being Morphism of c,c9 st g = T . f )
let g be Morphism of T . c,T . c9; :: thesis: ( Hom c,c9 <> {} & ex f being Morphism of c,c9 st g = T . f )
g in Hom (T . c),(T . c9) by A8, Def7;
then g in rng (hom T,c,c9) by A7;
then consider f being set such that
A9: f in dom (hom T,c,c9) and
A10: (hom T,c,c9) . f = g by FUNCT_1:def 5;
thus Hom c,c9 <> {} by A9; :: thesis: ex f being Morphism of c,c9 st g = T . f
A11: f in Hom c,c9 by A8, A9, FUNCT_2:def 1;
then reconsider f = f as Morphism of c,c9 by Def7;
take f ; :: thesis: g = T . f
thus g = T . f by A10, A11, Th131; :: thesis: verum