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 x in sum F holds
x +* (i,g) in sum F
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 x in sum F holds
x +* (i,g) in sum F
let x be Function; :: thesis: for i being Element of I
for g being Element of (F . i) st x in sum F holds
x +* (i,g) in sum F
let i be Element of I; :: thesis: for g being Element of (F . i) st x in sum F holds
x +* (i,g) in sum F
let g be Element of (F . i); :: thesis: ( x in sum F implies x +* (i,g) in sum F )
set y = x +* (i,g);
assume A1: x in sum F ; :: thesis: x +* (i,g) in sum F
then A2: x +* (i,g) in product F by Th24, GROUP_2:40;
for j being object st j in support ((x +* (i,g)),F) holds
j in (support (x,F)) \/ {i}

proof

let j be object ; :: thesis: ( j in support ((x +* (i,g)),F) implies j in (support (x,F)) \/ {i} )
assume j in support ((x +* (i,g)),F) ; :: thesis: j in (support (x,F)) \/ {i}
then consider Z being Group such that
A3: ( Z = F . j & (x +* (i,g)) . 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 TARSKI:def 3, XBOOLE_1:7; :: thesis: verum

end;

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

then ( x . j <> 1_ Z & j in I ) by A3, FUNCT_7:32;
then j in support (x,F) by A3, Def1;
hence j in (support (x,F)) \/ {i} by TARSKI:def 3, XBOOLE_1:7; :: thesis: verum

end;

end;

end;

then support ((x +* (i,g)),F) c= (support (x,F)) \/ {i} ;
hence x +* (i,g) in sum F by A1, A2, Th8; :: thesis: verum