let I be non empty set ; :: thesis: 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}
let G be Group; :: thesis: 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}
let i be Element of I; :: thesis: 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}
let g be Element of G; :: thesis: for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) & g <> 1_ G holds
support a = {i}
let a be Function of I,G; :: thesis: ( a = (I --> (1_ G)) +* (i,g) & g <> 1_ G implies support a = {i} )
assume that
A1: a = (I --> (1_ G)) +* (i,g) and
A2: g <> 1_ G ; :: thesis: support a = {i}
A3: support a c= {i} by A1, Th19;
dom (I --> (1_ G)) = I by FUNCOP_1:13;
then a . i = g by A1, FUNCT_7:31;
then i in support a by A2, Def2;
then {i} c= support a by ZFMISC_1:31;
hence support a = {i} by A3, XBOOLE_0:def 10; :: thesis: verum