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

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