let I be non empty set ; :: thesis: for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let F be component-commutative Subgroup-Family of I,G; :: thesis: for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let UF be Subset of G; :: thesis: for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let y be finite-support Function of I,(gr UF); :: thesis: for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let i be Element of I; :: thesis: for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let g be Element of (gr UF); :: thesis: ( y in product F & y . i = 1_ (F . i) & g in F . i implies (Product y) * g = g * (Product y) )

assume that

A1: y in product F and

A2: y . i = 1_ (F . i) and

A3: g in F . i ; :: thesis: (Product y) * g = g * (Product y)

reconsider x = y +* (i,g) as finite-support Function of I,(gr UF) by GROUP_19:26;

A4: y = x +* (i,(1_ (F . i))) by A2, Th7;

A5: x in product F by A1, A3, GROUP_19:24;

dom y = I by PARTFUN1:def 2;

then x . i = g by FUNCT_7:31;

hence (Product y) * g = g * (Product y) by A4, A5, Th9; :: thesis: verum

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let F be component-commutative Subgroup-Family of I,G; :: thesis: for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let UF be Subset of G; :: thesis: for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let y be finite-support Function of I,(gr UF); :: thesis: for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let i be Element of I; :: thesis: for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

let g be Element of (gr UF); :: thesis: ( y in product F & y . i = 1_ (F . i) & g in F . i implies (Product y) * g = g * (Product y) )

assume that

A1: y in product F and

A2: y . i = 1_ (F . i) and

A3: g in F . i ; :: thesis: (Product y) * g = g * (Product y)

reconsider x = y +* (i,g) as finite-support Function of I,(gr UF) by GROUP_19:26;

A4: y = x +* (i,(1_ (F . i))) by A2, Th7;

A5: x in product F by A1, A3, GROUP_19:24;

dom y = I by PARTFUN1:def 2;

then x . i = g by FUNCT_7:31;

hence (Product y) * g = g * (Product y) by A4, A5, Th9; :: thesis: verum