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

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