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 :: thesis: ( Hom ((T . c),(T . c9)) <> {} implies rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )

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

proof

let g be object ; :: 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 object such that
A3: f in dom (hom (T,c,c9)) and
A4: (hom (T,c,c9)) . f = g by FUNCT_1:def 3;
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:5; :: 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 Def3;
then consider f being Morphism of c,c9 such that
A5: g = T . f by A1, A2;
Hom (c,c9) <> {} by A1, A2;
then f in Hom (c,c9) by Def3;
then (hom (T,c,c9)) . f in rng (hom (T,c,c9)) by A2, FUNCT_2:4;
hence g in rng (hom (T,c,c9)) by A5, A1, A2, Th83; :: 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 A6: 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 26 :: 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 A7: 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 A7, Def3;
then g in rng (hom (T,c,c9)) by A6;
then consider f being object such that
A8: f in dom (hom (T,c,c9)) and
A9: (hom (T,c,c9)) . f = g by FUNCT_1:def 3;
thus Hom (c,c9) <> {} by A8; :: thesis: ex f being Morphism of c,c9 st g = T . f
A10: f in Hom (c,c9) by A7, A8, FUNCT_2:def 1;
then reconsider f = f as Morphism of c,c9 by Def3;
take f ; :: thesis: g = T . f
thus g = T . f by A9, A10, Th83; :: thesis: verum