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
A1: the MorphMap of (incl C) = id the Arrows of C by FUNCTOR0:def 29;
let a, b be object of C; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (incl C) . f = f )
assume A2: <^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
A3: [a,b] in [:the carrier of C,the carrier of C:] by ZFMISC_1:def 2;
<^((incl C) . a),((incl C) . b)^> <> {} by A2, FUNCTOR0:29, XBOOLE_1:3;
hence (incl C) . f = (Morph-Map (incl C),a,b) . f by A2, FUNCTOR0:def 16
.= (id (the Arrows of C . a,b)) . f by A1, A3, MSUALG_3:def 1
.= f by A2, FUNCT_1:35 ;
:: thesis: verum