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

proof

let j be object ; :: thesis: ( j in support (y,F) implies j in (support (x,F)) \/ {i} )
assume j in support (y,F) ; :: thesis: j in (support (x,F)) \/ {i}
then A2: ex Z being Group st
( Z = F . j & y . j <> 1_ Z & j in I ) by Def1;

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

suppose j = i ; :: thesis: j in (support (x,F)) \/ {i}

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

end;

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

then y . j = x . j by FUNCT_7:32;
then j in support (x,F) by A2, Def1;
hence j in (support (x,F)) \/ {i} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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