let I be non empty set ; 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; 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; 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; 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); ( x in product F implies x +* (i,g) in product F )
assume A1:
x in product F
; 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
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; verum