let C be Category; :: thesis: for E being Subcategory of C
for f being Morphism of holds f is Morphism of
let E be Subcategory of C; :: thesis: for f being Morphism of holds f is Morphism of
let f be Morphism of ; :: thesis: f is Morphism of
( f in the carrier' of E & the carrier' of E c= the carrier' of C ) by Th13;
hence f is Morphism of ; :: thesis: verum