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