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

let E be Subcategory of C; :: thesis: incl E is faithful

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

( not (incl E) . b_{1} = (incl E) . b_{2} or b_{1} = b_{2} ) )

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

( not (incl E) . b_{1} = (incl E) . b_{2} or b_{1} = b_{2} )

let f1, f2 be Morphism of a,b; :: thesis: ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 )

(incl E) . f1 = f1 by FUNCT_1:18;

hence ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 ) by FUNCT_1:18; :: thesis: verum

let E be Subcategory of C; :: thesis: incl E is faithful

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

( not (incl E) . b

assume Hom (a,b) <> {} ; :: thesis: for b

( not (incl E) . b

let f1, f2 be Morphism of a,b; :: thesis: ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 )

(incl E) . f1 = f1 by FUNCT_1:18;

hence ( not (incl E) . f1 = (incl E) . f2 or f1 = f2 ) by FUNCT_1:18; :: thesis: verum