let C be Category; :: thesis: for E being Subcategory of C holds
( incl E is full iff for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b' )
let E be Subcategory of C; :: thesis: ( incl E is full iff for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b' )
set T = incl E;
thus ( incl E is full implies for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b' ) :: thesis: ( ( for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b' ) implies incl E is full )

proof

assume A1: for a, b being Object of st Hom ((incl E) . a),((incl E) . b) <> {} holds
for g being Morphism of (incl E) . a,(incl E) . b holds
( Hom a,b <> {} & ex f being Morphism of a,b st g = (incl E) . f ) ; :: according to CAT_1:def 23 :: thesis: for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b'
let a, b be Object of ; :: thesis: for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b'
let a', b' be Object of ; :: thesis: ( a = a' & b = b' implies Hom a,b = Hom a',b' )
assume A2: ( a = a' & b = b' ) ; :: thesis: Hom a,b = Hom a',b'

now

let x be set ; :: thesis: ( ( x in Hom a,b implies x in Hom a',b' ) & ( x in Hom a',b' implies x in Hom a,b ) )
Hom a,b c= Hom a',b' by A2, Def4;
hence ( x in Hom a,b implies x in Hom a',b' ) ; :: thesis: ( x in Hom a',b' implies x in Hom a,b )
assume A3: x in Hom a',b' ; :: thesis: x in Hom a,b
A4: ( (incl E) . a = a' & (incl E) . b = b' ) by A2, Th22;
then reconsider g = x as Morphism of (incl E) . a,(incl E) . b by A3, CAT_1:def 7;
consider f being Morphism of a,b such that
A5: g = (incl E) . f by A1, A4, A3;
A6: g = f by A5, FUNCT_1:35;
Hom a,b <> {} by A1, A4, A3;
hence x in Hom a,b by A6, CAT_1:def 7; :: thesis: verum

end;

hence Hom a,b = Hom a',b' by TARSKI:2; :: thesis: verum

end;

assume A7: for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b' ; :: thesis: incl E is full
let a, b be Object of ; :: according to CAT_1:def 23 :: thesis: ( Hom ((incl E) . a),((incl E) . b) = {} or for b₁ being Morphism of (incl E) . a,(incl E) . b holds
( not Hom a,b = {} & ex b₂ being Morphism of a,b st b₁ = (incl E) . b₂ ) )
assume A8: Hom ((incl E) . a),((incl E) . b) <> {} ; :: thesis: for b₁ being Morphism of (incl E) . a,(incl E) . b holds
( not Hom a,b = {} & ex b₂ being Morphism of a,b st b₁ = (incl E) . b₂ )
let g be Morphism of (incl E) . a,(incl E) . b; :: thesis: ( not Hom a,b = {} & ex b₁ being Morphism of a,b st g = (incl E) . b₁ )
A9: g in Hom ((incl E) . a),((incl E) . b) by A8, CAT_1:def 7;
A10: ( a = (incl E) . a & b = (incl E) . b ) by Th22;
hence Hom a,b <> {} by A7, A8; :: thesis: ex b₁ being Morphism of a,b st g = (incl E) . b₁
Hom a,b = Hom ((incl E) . a),((incl E) . b) by A7, A10;
then reconsider f = g as Morphism of a,b by A9, CAT_1:def 7;
take f ; :: thesis: g = (incl E) . f
thus g = (incl E) . f by FUNCT_1:35; :: thesis: verum