let G, H be Group; :: thesis: Image (1: G,H) = (1). H
set g = 1: G,H;
A1: the carrier of (Image (1: G,H)) c= {(1_ H)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Image (1: G,H)) or x in {(1_ H)} )
assume x in the carrier of (Image (1: G,H)) ; :: thesis: x in {(1_ H)}
then x in (1: G,H) .: the carrier of G by Def11;
then consider y being set such that
y in dom (1: G,H) and
A2: y in the carrier of G and
A3: (1: G,H) . y = x by FUNCT_1:def 12;
reconsider y = y as Element of G by A2;
(1: G,H) . y = 1_ H by Def8;
hence x in {(1_ H)} by A3, TARSKI:def 1; :: thesis: verum

end;

1_ H in Image (1: G,H) by GROUP_2:55;
then 1_ H in the carrier of (Image (1: G,H)) by STRUCT_0:def 5;
then {(1_ H)} c= the carrier of (Image (1: G,H)) by ZFMISC_1:37;
then the carrier of (Image (1: G,H)) = {(1_ H)} by A1, XBOOLE_0:def 10;
hence Image (1: G,H) = (1). H by GROUP_2:def 7; :: thesis: verum