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 )
proof
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)
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) ) )
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;
hence Hom (a,b) = Hom (a9,b9) by TARSKI:2; :: thesis: verum
end;
assume A7: 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: 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 b1 being Morphism of (incl E) . a,(incl E) . b holds
( not Hom (a,b) = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 ) )
assume A8: Hom (((incl E) . a),((incl E) . b)) <> {} ; :: thesis: for b1 being Morphism of (incl E) . a,(incl E) . b holds
( not Hom (a,b) = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 )
let g be Morphism of (incl E) . a,(incl E) . b; :: thesis: ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st g = (incl E) . b1 )
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 b1 being Morphism of a,b st g = (incl E) . b1
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