let A be category; :: thesis: for C being non empty subcategory of A
for a, b being Object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds (incl C) . f = f
let C be non empty subcategory of A; :: thesis: for a, b being Object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds (incl C) . f = f
let a, b be Object of C; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (incl C) . f = f )
assume A1: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (incl C) . f = f
let f be Morphism of a,b; :: thesis: (incl C) . f = f
A2: ( the MorphMap of (incl C) = id the Arrows of C & [a,b] in [: the carrier of C, the carrier of C:] ) by FUNCTOR0:def 28, ZFMISC_1:def 2;
<^((incl C) . a),((incl C) . b)^> <> {} by A1, FUNCTOR0:28, XBOOLE_1:3;
hence (incl C) . f = (Morph-Map ((incl C),a,b)) . f by A1, FUNCTOR0:def 15
.= (id ( the Arrows of C . (a,b))) . f by A2, MSUALG_3:def 1
.= f ;
:: thesis: verum