let I be non empty set ; :: thesis: for G being Group
for a being Function of I,G
for i being Element of I
for g being Element of G st support a is finite holds
support (a +* (i,g)) is finite
let G be Group; :: thesis: for a being Function of I,G
for i being Element of I
for g being Element of G st support a is finite holds
support (a +* (i,g)) is finite
let a be Function of I,G; :: thesis: for i being Element of I
for g being Element of G st support a is finite holds
support (a +* (i,g)) is finite
let i be Element of I; :: thesis: for g being Element of G st support a is finite holds
support (a +* (i,g)) is finite
let g be Element of G; :: thesis: ( support a is finite implies support (a +* (i,g)) is finite )
reconsider b = a +* (i,g) as Function of I,G ;
assume A1: support a is finite ; :: thesis: support (a +* (i,g)) is finite
for j being object st j in support b holds
j in (support a) \/ {i}

proof

let j be object ; :: thesis: ( j in support b implies j in (support a) \/ {i} )
assume j in support b ; :: thesis: j in (support a) \/ {i}
then A2: ( b . j <> 1_ G & j in I ) by Def2;

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: j in (support a) \/ {i}

then j in {i} by TARSKI:def 1;
hence j in (support a) \/ {i} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose i <> j ; :: thesis: j in (support a) \/ {i}

then b . j = a . j by FUNCT_7:32;
then j in support a by A2, Def2;
hence j in (support a) \/ {i} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then support b c= (support a) \/ {i} ;
hence support (a +* (i,g)) is finite by A1; :: thesis: verum