let G, H be strict 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 by GROUP_2:def 5;
A2: the carrier of (Image (h | A)) = rng (h | A) by GROUP_6:53
.= h .: the carrier of A by RELAT_1:148 ;
h .: the carrier of G = the carrier of (Image h) by GROUP_6:def 11;
hence Image (h | A) is strict Subgroup of Image h by A1, A2, GROUP_2:66, RELAT_1:156; :: thesis: verum