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