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) holds
support a c= {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) holds
support a c= {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) holds
support a c= {i}
let g be Element of G; :: thesis: for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) holds
support a c= {i}
let a be Function of I,G; :: thesis: ( a = (I --> (1_ G)) +* (i,g) implies support a c= {i} )
assume A1: a = (I --> (1_ G)) +* (i,g) ; :: thesis: support a c= {i}
for j being object st j in support a holds
j in {i}

proof

let j be object ; :: thesis: ( j in support a implies j in {i} )
assume A2: j in support a ; :: thesis: j in {i}
j = i

proof

assume j <> i ; :: thesis: contradiction
then a . j = (I --> (1_ G)) . j by A1, FUNCT_7:32
.= 1_ G by A2, FUNCOP_1:7 ;
hence contradiction by A2, Def2; :: thesis: verum

end;

hence j in {i} by TARSKI:def 1; :: thesis: verum

end;

hence support a c= {i} ; :: thesis: verum