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 A2: 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
A3: f in dom (hom T,c,c') and
A4: (hom T,c,c') . f = g by FUNCT_1:def 5;
f in Hom c,c' by A2, A3, FUNCT_2:def 1;
hence g in Hom (T . c),(T . c') by A2, A4, 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
A5: g = T . f by A1, A2, Def23;
A6: Hom c,c' <> {} by A1, A2, Def23;
then f in Hom c,c' by Def7;
then (hom T,c,c') . f in rng (hom T,c,c') by A2, FUNCT_2:6;
hence g in rng (hom T,c,c') by A5, A6, 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 A7: 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 A8: 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 A8, Def7;
then g in rng (hom T,c,c') by A7;
then consider f being set such that
A9: f in dom (hom T,c,c') and
A10: (hom T,c,c') . f = g by FUNCT_1:def 5;
thus Hom c,c' <> {} by A9; :: thesis: ex f being Morphism of c,c' st g = T . f
A11: f in Hom c,c' by A8, A9, FUNCT_2:def 1;
then reconsider f = f as Morphism of c,c' by Def7;
take f ; :: thesis: g = T . f
thus g = T . f by A10, A11, Th131; :: thesis: verum