theorem Th20: :: GROUP_19:20

for I being non empty set
for G being Group
for i being Element of I
for g being Element of G
for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) & g <> 1_ G holds
support a = {i}