let G, H be Group; :: thesis: for h being Homomorphism of G,H
for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h
let h be Homomorphism of G,H; :: thesis: for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h
let A be strict Subgroup of G; :: thesis: Image (h | A) is strict Subgroup of Image h
A1: ( the carrier of A c= the carrier of G & h .: the carrier of G = the carrier of (Image h) ) by GROUP_2:def 5, GROUP_6:def 10;
the carrier of (Image (h | A)) = rng (h | A) by GROUP_6:44
.= h .: the carrier of A by RELAT_1:115 ;
hence Image (h | A) is strict Subgroup of Image h by A1, GROUP_2:57, RELAT_1:123; :: thesis: verum