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 product F holds
x +* (i,g) in product 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 product F holds
x +* (i,g) in product F
let x be Function; :: thesis: for i being Element of I
for g being Element of (F . i) st x in product F holds
x +* (i,g) in product F
let i be Element of I; :: thesis: for g being Element of (F . i) st x in product F holds
x +* (i,g) in product F
let g be Element of (F . i); :: thesis: ( x in product F implies x +* (i,g) in product F )
assume A1: x in product F ; :: thesis: x +* (i,g) in product F
then A2: x in product (Carrier F) by GROUP_7:def 2;
then A3: ( dom x = dom (Carrier F) & ( for j being object st j in dom (Carrier F) holds
x . j in (Carrier F) . j ) ) by CARD_3:9;
A4: dom x = I by A1, Th3;
set y = x +* (i,g);
A6: dom (x +* (i,g)) = I by A4, FUNCT_7:30;
A7: for j being object st j in dom (Carrier F) holds
(x +* (i,g)) . j in (Carrier F) . j

proof

let j be object ; :: thesis: ( j in dom (Carrier F) implies (x +* (i,g)) . j in (Carrier F) . j )
assume A8: j in dom (Carrier F) ; :: thesis: (x +* (i,g)) . j in (Carrier F) . j

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

suppose A9: j = i ; :: thesis: (x +* (i,g)) . j in (Carrier F) . j

then A10: (x +* (i,g)) . j = g by A4, FUNCT_7:31;
g in [#] (F . i) ;
hence (x +* (i,g)) . j in (Carrier F) . j by A9, A10, PENCIL_3:7; :: thesis: verum

end;

suppose j <> i ; :: thesis: (x +* (i,g)) . j in (Carrier F) . j

then (x +* (i,g)) . j = x . j by FUNCT_7:32;
hence (x +* (i,g)) . j in (Carrier F) . j by A2, A8, CARD_3:9; :: thesis: verum

end;

end;

end;

x +* (i,g) in product (Carrier F) by A3, A4, A6, A7, CARD_3:9;
hence x +* (i,g) in product F by GROUP_7:def 2; :: thesis: verum