let I be non empty set ; :: thesis: for G being Group
for a being finite-support Function of I,G
for i being Element of I
for g being Element of G holds a +* (i,g) is finite-support Function of I,G
let G be Group; :: thesis: for a being finite-support Function of I,G
for i being Element of I
for g being Element of G holds a +* (i,g) is finite-support Function of I,G
let a be finite-support Function of I,G; :: thesis: for i being Element of I
for g being Element of G holds a +* (i,g) is finite-support Function of I,G
let i be Element of I; :: thesis: for g being Element of G holds a +* (i,g) is finite-support Function of I,G
let g be Element of G; :: thesis: a +* (i,g) is finite-support Function of I,G
reconsider b = a +* (i,g) as Function of I,G ;
support a is finite ;
then support b is finite by Th23;
hence a +* (i,g) is finite-support Function of I,G by Def3; :: thesis: verum