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