let C be Category; :: thesis: for E being Subcategory of C holds

( incl E is full iff for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) )

let E be Subcategory of C; :: thesis: ( incl E is full iff for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) )

set T = incl E;

thus ( incl E is full implies for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) ) :: thesis: ( ( for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) ) implies incl E is full )

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) ; :: thesis: incl E is full

let a, b be Object of E; :: according to CAT_1:def 26 :: thesis: ( Hom (((incl E) . a),((incl E) . b)) = {} or for b_{1} being Morphism of (incl E) . a,(incl E) . b holds

( not Hom (a,b) = {} & ex b_{2} being Morphism of a,b st b_{1} = (incl E) . b_{2} ) )

assume A8: Hom (((incl E) . a),((incl E) . b)) <> {} ; :: thesis: for b_{1} being Morphism of (incl E) . a,(incl E) . b holds

( not Hom (a,b) = {} & ex b_{2} being Morphism of a,b st b_{1} = (incl E) . b_{2} )

let g be Morphism of (incl E) . a,(incl E) . b; :: thesis: ( not Hom (a,b) = {} & ex b_{1} being Morphism of a,b st g = (incl E) . b_{1} )

A9: g in Hom (((incl E) . a),((incl E) . b)) by A8, CAT_1:def 5;

A10: ( a = (incl E) . a & b = (incl E) . b ) by Th10;

hence Hom (a,b) <> {} by A7, A8; :: thesis: ex b_{1} being Morphism of a,b st g = (incl E) . b_{1}

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 5;

take f ; :: thesis: g = (incl E) . f

thus g = (incl E) . f by FUNCT_1:18; :: thesis: verum

( incl E is full iff for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) )

let E be Subcategory of C; :: thesis: ( incl E is full iff for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) )

set T = incl E;

thus ( incl E is full implies for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) ) :: thesis: ( ( for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) ) implies incl E is full )

proof

assume A7:
for a, b being Object of E
assume A1:
for a, b being Object of E 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 26 :: thesis: for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9)

let a, b be Object of E; :: thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9)

let a9, b9 be Object of C; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )

assume A2: ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) = Hom (a9,b9)

end;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 26 :: thesis: for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9)

let a, b be Object of E; :: thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9)

let a9, b9 be Object of C; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )

assume A2: ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) = Hom (a9,b9)

now :: thesis: for x being object holds

( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )

hence
Hom (a,b) = Hom (a9,b9)
by TARSKI:2; :: thesis: verum( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )

let x be object ; :: thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )

Hom (a,b) c= Hom (a9,b9) by A2, Def4;

hence ( x in Hom (a,b) implies x in Hom (a9,b9) ) ; :: thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )

assume A3: x in Hom (a9,b9) ; :: thesis: x in Hom (a,b)

A4: ( (incl E) . a = a9 & (incl E) . b = b9 ) by A2, Th10;

then reconsider g = x as Morphism of (incl E) . a,(incl E) . b by A3, CAT_1:def 5;

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:18;

Hom (a,b) <> {} by A1, A4, A3;

hence x in Hom (a,b) by A6, CAT_1:def 5; :: thesis: verum

end;Hom (a,b) c= Hom (a9,b9) by A2, Def4;

hence ( x in Hom (a,b) implies x in Hom (a9,b9) ) ; :: thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )

assume A3: x in Hom (a9,b9) ; :: thesis: x in Hom (a,b)

A4: ( (incl E) . a = a9 & (incl E) . b = b9 ) by A2, Th10;

then reconsider g = x as Morphism of (incl E) . a,(incl E) . b by A3, CAT_1:def 5;

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:18;

Hom (a,b) <> {} by A1, A4, A3;

hence x in Hom (a,b) by A6, CAT_1:def 5; :: thesis: verum

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) ; :: thesis: incl E is full

let a, b be Object of E; :: according to CAT_1:def 26 :: thesis: ( Hom (((incl E) . a),((incl E) . b)) = {} or for b

( not Hom (a,b) = {} & ex b

assume A8: Hom (((incl E) . a),((incl E) . b)) <> {} ; :: thesis: for b

( not Hom (a,b) = {} & ex b

let g be Morphism of (incl E) . a,(incl E) . b; :: thesis: ( not Hom (a,b) = {} & ex b

A9: g in Hom (((incl E) . a),((incl E) . b)) by A8, CAT_1:def 5;

A10: ( a = (incl E) . a & b = (incl E) . b ) by Th10;

hence Hom (a,b) <> {} by A7, A8; :: thesis: ex 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 5;

take f ; :: thesis: g = (incl E) . f

thus g = (incl E) . f by FUNCT_1:18; :: thesis: verum