theorem :: GROUP_3:53

for G being Group
for A being Subset of G st A <> {} holds
(1_ G) |^ A = {(1_ G)}