let G be Group; :: thesis: for H being strict Subgroup of G holds Image (incl H) = H
let H be strict Subgroup of G; :: thesis: Image (incl H) = H
the carrier of H c= the carrier of H ;
then the carrier of H = (id the carrier of H) .: the carrier of H by FUNCT_1:92
.= (incl H) .: the carrier of H by Def9
.= the carrier of (Image (incl H)) by GROUP_6:def 10 ;
hence Image (incl H) = H by GROUP_2:59; :: thesis: verum