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