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

proof

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

now

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

proof

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

proof

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

end;

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

end;

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

end;

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

end;

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